1  /-
  2  Copyright (c) 2018 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Mario Carneiro
  5  
  6  Godel numbering for partial recursive functions.
  7  -/
  8  import computability.partrec
src         └───────────────────┘
  9  
 10  open encodable denumerable
 11  
 12  namespace nat.partrec
 13  open nat (mkpair)
 14  
 15  theorem rfind' {f} (hf : nat.partrec f) : nat.partrec (nat.unpaired (λ a m,
id                            └─────────┘     └─────────┘  └──────────┘     
src                           └─────────┘      └─────────┘  └──────────┘
typ                           └─────────┘     └─────────┘  └──────────┘     
 16    (nat.rfind (λ n, (λ m, m = 0) <$> f (mkpair a (n + m)))).map (+ m))) :=
id      └───────┘                └─┘   └────┘         └─┘    
src     └───────┘                   └─┘    └────┘            └─┘  
typ     └───────┘                └─┘   └────┘         └─┘    
doc                                         └────┘             └─┘
 17  partrec₂.unpaired'.2 $
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
 18  begin
st   └─────
 19    refine partrec.map
id            └─────────┘
src    └─────┘└─────────┘
typ    └─────┘└─────────┘
doc    └─────┘           
txt    └─────┘           
par    └─────┘           
pid                     
st   ─────────────────────
 20      ((@partrec₂.unpaired' (λ (a b : ℕ),
id          └────────────────┘
src  ───┘   └────────────────┘  └──────┘ └──
typ  ───┘   └────────────────┘  └──────┘ └──
doc  ───┘                       └──────┘ └──
txt  ───┘                       └──────┘ └──
par  ───┘                       └──────┘ └──
pid  ───┘                       └──────┘ └──
st   ────────────────────────────────────────
 21        nat.rfind (λ n, (λ m, m = 0) <$> f (mkpair a (n + b))))).1 _)
id         └───────┘                   └─┘   └────┘      
src  ─────┘└───────┘  └──┘  └──┘ └──┘└─┘  └────┘    └──────────
typ  ─────┘└───────┘  └──┘  └──┘ └──┘└─┘ └────┘    └──────────
doc  ─────┘           └──┘  └──┘  └──┘     └────┘     └──────────
txt  ─────┘           └──┘  └──┘  └──┘                └──────────
par  ─────┘           └──┘  └──┘  └──┘                └──────────
pid  ─────┘           └──┘  └──┘  └──┘                └──────────
st   ────────────────────────────────────────────────────────────────────
 22      (primrec.nat_add.comp primrec.snd $
id        └──────────────────┘
src  ───┘ └──────────────────┘            
typ  ───┘ └──────────────────┘            
doc  ───┘                                 
txt  ───┘                                 
par  ───┘                                 
pid  ───┘                                 
st   ────────────────────────────────────────
 23        primrec.snd.comp primrec.fst).to_comp.to₂,
id         └──────────────┘ └─────────┘
src  ─────┘└──────────────┘└─────────┘└───────────┘
typ  ─────┘└──────────────┘└─────────┘└───────────┘
doc  ─────┘                           └───────────┘
txt  ─────┘                           └───────────┘
par  ─────┘                           └───────────┘
pid  ─────┘                           └──────────┘
st   ──────────────────────────────────────────────┘└─
 24    have := rfind (partrec₂.unpaired'.2 ((partrec.nat_iff.2 hf).comp
id             └───┘  └────────────────┘     └─────────────┘   └┘
src    └──────┘└───┘ └────────────────┘└─┘  └─────────────┘└─┘  └──────
typ    └──────┘└───┘ └────────────────┘└─┘  └─────────────┘└─┘└┘└──────
doc    └──────┘                        └─┘                 └─┘  └──────
txt    └──────┘                        └─┘                 └─┘  └──────
par    └──────┘                        └─┘                 └─┘  └──────
pid    └───┘└─┘                        └─┘                 └─┘  └──────
st   ───────────────────────────────────────────────────────────────────
 25      (primrec₂.mkpair.comp
id        └──────────────────┘
src  ───┘ └──────────────────┘
typ  ───┘ └──────────────────┘
doc  ───┘                     
txt  ───┘                     
par  ───┘                     
pid  ───┘                     
st   ──────────────────────────
 26        (primrec.fst.comp $ primrec.unpair.comp primrec.fst)
id          └──────────────┘
src  ─────┘ └──────────────┘                               └─
typ  ─────┘ └──────────────┘                               └─
doc  ─────┘                                                └─
txt  ─────┘                                                └─
par  ─────┘                                                └─
pid  ─────┘                                                └─
st   ───────────────────────────────────────────────────────────
 27        (primrec.nat_add.comp primrec.snd
id          └──────────────────┘
src  ─────┘ └──────────────────┘           
typ  ─────┘ └──────────────────┘           
doc  ─────┘                                
txt  ─────┘                                
par  ─────┘                                
pid  ─────┘                                
st   ────────────────────────────────────────
 28          (primrec.snd.comp $ primrec.unpair.comp primrec.fst))).to_comp).to₂),
id            └──────────────┘   └─────────────────┘ └─────────┘
src  ───────┘ └──────────────┘ └─────────────────┘└─────────┘└───────────────┘
typ  ───────┘ └──────────────┘ └─────────────────┘└─────────┘└───────────────┘
doc  ───────┘                                                └───────────────┘
txt  ───────┘                                                └───────────────┘
par  ───────┘                                                └───────────────┘
pid  ───────┘                                                └───────────────┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
 29    simp at this, exact this
id                         └──┘
src    └──────────┘  └────┘    
typ    └──────────┘  └────┘└──┘
doc    └──────────┘  └────┘    
txt    └──────────┘  └────┘    
par    └──────────┘  └────┘    
pid        └─────┘           
st   ─────────────┘└───────────┘
 30  end
st   └─┘
 31  
 32  inductive code : Type
 33  | zero : code
 34  | succ : code
 35  | left : code
 36  | right : code
 37  | pair : code → code → code
 38  | comp : code → code → code
 39  | prec : code → code → code
 40  | rfind' : code → code
 41  
 42  end nat.partrec
 43  
 44  namespace nat.partrec.code
 45  open nat (mkpair unpair)
 46  open nat.partrec (code)
 47  
 48  instance : inhabited code := ⟨zero⟩
id              └───────┘ └──┘     └──┘
src             └───────┘ └──┘     └──┘
typ             └───────┘ └──┘     └──┘
 49  
 50  protected def const : ℕ → code
id                           └──┘
src                           └──┘
typ                          └──┘
 51  | 0     := zero
id              └──┘
src             └──┘
typ             └──┘
 52  | (n+1) := comp succ (const n)
id            └──┘ └──┘  └───┘
src            └──┘ └──┘
typ           └──┘ └──┘  └───┘
 53  
 54  protected def id : code := pair left right
id                      └──┘    └──┘ └──┘ └───┘
src                     └──┘    └──┘ └──┘ └───┘
typ                     └──┘    └──┘ └──┘ └───┘
 55  
 56  def curry (c : code) (n : ℕ) : code :=
id                  └──┘           └──┘
src                 └──┘           └──┘
typ                 └──┘           └──┘
 57  comp c (pair (code.const n) code.id)
id   └──┘   └──┘  └────────┘   └─────┘
src  └──┘    └──┘  └────────┘    └─────┘
typ  └──┘   └──┘  └────────┘   └─────┘
 58  
 59  def encode_code : code → ℕ
id                     └──┘  
src                    └──┘   
typ                    └──┘  
 60  | zero         := 0
id     └──┘
src    └──┘
typ    └──┘
 61  | succ         := 1
id     └──┘
src    └──┘
typ    └──┘
 62  | left         := 2
id     └──┘
src    └──┘
typ    └──┘
 63  | right        := 3
id     └───┘
src    └───┘
typ    └───┘
 64  | (pair cf cg) := bit0 (bit0 $ mkpair (encode_code cf) (encode_code cg)) + 4
id      └──┘ └┘ └┘     └──┘  └──┘   └────┘  └─────────┘      └─────────┘      
src     └──┘           └──┘  └──┘   └────┘                                    
typ     └──┘ └┘ └┘     └──┘  └──┘   └────┘  └─────────┘      └─────────┘      
doc                                 └────┘
 65  | (comp cf cg) := bit0 (bit1 $ mkpair (encode_code cf) (encode_code cg)) + 4
id      └──┘ └┘ └┘     └──┘  └──┘   └────┘  └─────────┘      └─────────┘      
src     └──┘           └──┘  └──┘   └────┘                                    
typ     └──┘ └┘ └┘     └──┘  └──┘   └────┘  └─────────┘      └─────────┘      
doc                                 └────┘
 66  | (prec cf cg) := bit1 (bit0 $ mkpair (encode_code cf) (encode_code cg)) + 4
id      └──┘ └┘ └┘     └──┘  └──┘   └────┘  └─────────┘      └─────────┘      
src     └──┘           └──┘  └──┘   └────┘                                    
typ     └──┘ └┘ └┘     └──┘  └──┘   └────┘  └─────────┘      └─────────┘      
doc                                 └────┘
 67  | (rfind' cf)  := bit1 (bit1 $ encode_code cf) + 4
id      └────┘ └┘      └──┘  └──┘   └─────────┘     
src     └────┘         └──┘  └──┘                   
typ     └────┘ └┘      └──┘  └──┘   └─────────┘     
 68  
 69  def of_nat_code : ℕ → code
id                       └──┘
src                       └──┘
typ                      └──┘
 70  | 0     := zero
id              └──┘
src             └──┘
typ             └──┘
 71  | 1     := succ
id              └──┘
src             └──┘
typ             └──┘
 72  | 2     := left
id              └──┘
src             └──┘
typ             └──┘
 73  | 3     := right
id              └───┘
src             └───┘
typ             └───┘
 74  | (n+4) := let m := n.div2.div2 in
id                     └────────┘
src                      └────────┘
typ                    └────────┘
 75    have hm : m < n + 4, by simp [m, nat.div2_val];
id                                  └──────────┘
src                          └────┘ └┘└──────────┘
typ                         └────┘└┘└──────────┘
doc                            └────┘ └┘            
txt                            └────┘ └┘            
par                            └────┘ └┘            
pid                                 └┘            
st                            └────────────────────────
 76    from lt_of_le_of_lt
id          └────────────┘
src    └───┘└────────────┘
typ    └───┘└────────────┘
doc    └───┘              
txt    └───┘              
par    └───┘              
pid    └───┘              
st   ──────────────────────
 77      (le_trans (nat.div_le_self _ _) (nat.div_le_self _ _))
id        └──────┘                        └─────────────┘
src  ───┘ └──────┘                └────┘ └─────────────┘└──────
typ  ───┘ └──────┘                └────┘ └─────────────┘└──────
doc  ───┘                         └────┘                └──────
txt  ───┘                         └────┘                └──────
par  ───┘                         └────┘                └──────
pid  ───┘                         └────┘                └──────
st   ───────────────────────────────────────────────────────────
 78      (nat.succ_le_succ (nat.le_add_right _ _)),
id        └──────────────┘  └──────────────┘
src  ───┘ └──────────────┘ └──────────────┘└────┘
typ  ───┘ └──────────────┘ └──────────────┘└────┘
doc  ───┘                                  └────┘
txt  ───┘                                  └────┘
par  ───┘                                  └────┘
pid  ───┘                                  └────┘
st   ────────────────────────────────────────────┘
 79    have m1 : m.unpair.1 < n + 4, from lt_of_le_of_lt m.unpair_le_left hm,
id               └─────┘              └────────────┘ └─────────────┘ └┘
src               └─────┘              └────────────┘  └─────────────┘
typ              └─────┘              └────────────┘ └─────────────┘ └┘
doc               └─────┘
 80    have m2 : m.unpair.2 < n + 4, from lt_of_le_of_lt m.unpair_le_right hm,
id               └─────┘              └────────────┘ └──────────────┘ └┘
src               └─────┘              └────────────┘  └──────────────┘
typ              └─────┘              └────────────┘ └──────────────┘ └┘
doc               └─────┘
 81    match n.bodd, n.div2.bodd with
id            └───┘   └───┘└───┘
src           └───┘   └───┘└───┘
typ           └───┘   └───┘└───┘
 82    | ff, ff := pair (of_nat_code m.unpair.1) (of_nat_code m.unpair.2)
id           └┘    └──┘  └─────────┘ └─────┘    └─────────┘ └─────┘
src          └┘    └──┘               └─────┘                 └─────┘
typ          └┘    └──┘  └─────────┘ └─────┘    └─────────┘ └─────┘
doc                                   └─────┘                  └─────┘
 83    | ff, tt := comp (of_nat_code m.unpair.1) (of_nat_code m.unpair.2)
id       └┘  └┘    └──┘  └─────────┘ └─────┘    └─────────┘ └─────┘
src      └┘  └┘    └──┘               └─────┘                 └─────┘
typ      └┘  └┘    └──┘  └─────────┘ └─────┘    └─────────┘ └─────┘
doc                                   └─────┘                  └─────┘
 84    | tt, ff := prec (of_nat_code m.unpair.1) (of_nat_code m.unpair.2)
id       └┘  └┘    └──┘  └─────────┘ └─────┘    └─────────┘ └─────┘
src      └┘  └┘    └──┘               └─────┘                 └─────┘
typ      └┘  └┘    └──┘  └─────────┘ └─────┘    └─────────┘ └─────┘
doc                                   └─────┘                  └─────┘
st           └┘
 85    | tt, tt := rfind' (of_nat_code m)
id           └┘    └────┘  └─────────┘ 
src          └┘    └────┘
typ          └┘    └────┘  └─────────┘ 
 86    end
 87  
 88  private theorem encode_of_nat_code : ∀ n, encode_code (of_nat_code n) = n
id                                            └─────────┘  └─────────┘    
src                                            └─────────┘  └─────────┘    
typ                                           └─────────┘  └─────────┘    
 89  | 0     := rfl
id              └─┘
src             └─┘
typ             └─┘
 90  | 1     := rfl
id              └─┘
src             └─┘
typ             └─┘
 91  | 2     := rfl
id              └─┘
src             └─┘
typ             └─┘
 92  | 3     := rfl
id              └─┘
src             └─┘
typ             └─┘
 93  | (n+4) := let m := n.div2.div2 in
id                     └────────┘
src                      └────────┘
typ                    └────────┘
 94    have hm : m < n + 4, by simp [m, nat.div2_val];
id                                  └──────────┘
src                          └────┘ └┘└──────────┘
typ                         └────┘└┘└──────────┘
doc                            └────┘ └┘            
txt                            └────┘ └┘            
par                            └────┘ └┘            
pid                                 └┘            
st                            └────────────────────────
 95    from lt_of_le_of_lt
id          └────────────┘
src    └───┘└────────────┘
typ    └───┘└────────────┘
doc    └───┘              
txt    └───┘              
par    └───┘              
pid    └───┘              
st   ──────────────────────
 96      (le_trans (nat.div_le_self _ _) (nat.div_le_self _ _))
id        └──────┘                        └─────────────┘
src  ───┘ └──────┘                └────┘ └─────────────┘└──────
typ  ───┘ └──────┘                └────┘ └─────────────┘└──────
doc  ───┘                         └────┘                └──────
txt  ───┘                         └────┘                └──────
par  ───┘                         └────┘                └──────
pid  ───┘                         └────┘                └──────
st   ───────────────────────────────────────────────────────────
 97      (nat.succ_le_succ (nat.le_add_right _ _)),
id        └──────────────┘  └──────────────┘
src  ───┘ └──────────────┘ └──────────────┘└────┘
typ  ───┘ └──────────────┘ └──────────────┘└────┘
doc  ───┘                                  └────┘
txt  ───┘                                  └────┘
par  ───┘                                  └────┘
pid  ───┘                                  └────┘
st   ────────────────────────────────────────────┘
 98    have m1 : m.unpair.1 < n + 4, from lt_of_le_of_lt m.unpair_le_left hm,
id               └─────┘              └────────────┘ └─────────────┘ └┘
src               └─────┘              └────────────┘  └─────────────┘
typ              └─────┘              └────────────┘ └─────────────┘ └┘
doc               └─────┘
 99    have m2 : m.unpair.2 < n + 4, from lt_of_le_of_lt m.unpair_le_right hm,
id               └─────┘              └────────────┘ └──────────────┘ └┘
src               └─────┘              └────────────┘  └──────────────┘
typ              └─────┘              └────────────┘ └──────────────┘ └┘
doc               └─────┘
100    have IH : _ := encode_of_nat_code m,
id                    └────────────────┘ 
typ                   └────────────────┘ 
101    have IH1 : _ := encode_of_nat_code m.unpair.1,
id                     └────────────────┘ └─────┘
src                                        └─────┘
typ                    └────────────────┘ └─────┘
doc                                        └─────┘
102    have IH2 : _ := encode_of_nat_code m.unpair.2,
id                     └────────────────┘ └─────┘
src                                        └─────┘
typ                    └────────────────┘ └─────┘
doc                                        └─────┘
103    begin
st     └─────
104      transitivity, swap,
src      └──────────┘  └──┘
typ      └──────────┘  └──┘
doc      └──────────┘  └──┘
txt      └──────────┘  └──┘
par      └──────────┘  └──┘
st   ───────────────┘└────┘└─
105      rw [← nat.bit_decomp n, ← nat.bit_decomp n.div2],
id             └────────────┘     └────────────┘ └────┘
src      └────┘└────────────┘ └──┘└────────────┘└────┘
typ      └────┘└────────────┘└──┘└────────────┘└────┘
doc      └────┘               └──┘                    
txt      └────┘               └──┘                    
par      └────┘               └──┘                    
pid        └──┘               └──┘                    
st   ─────────────────────────┘└───────────────────────┘└──
106      simp [encode_code, of_nat_code, -add_comm],
id             └─────────┘  └─────────┘
src      └────┘└─────────┘└┘└─────────┘└──────────┘
typ      └────┘└─────────┘└┘└─────────┘└──────────┘
doc      └────┘           └┘           └──────────┘
txt      └────┘           └┘           └──────────┘
par      └────┘           └┘           └──────────┘
pid                     └┘           └──────────┘
st   ─────────────────────────────────────────────┘└─
107      cases n.bodd; cases n.div2.bodd;
id             └────┘        └─────────┘
src      └────┘└────┘  └────┘└─────────┘
typ      └────┘└────┘  └────┘└─────────┘
doc      └────┘        └────┘
txt      └────┘        └────┘
par      └────┘        └────┘
pid                        
st   ─────────────────────────────────────
108        simp [encode_code, of_nat_code, -add_comm, IH, IH1, IH2, m, nat.bit]
id               └─────────┘  └─────────┘             └┘  └─┘  └─┘    └─────┘
src        └────┘└─────────┘└┘└─────────┘└───────────┘  └┘   └┘   └┘ └┘└─────┘└─
typ        └────┘└─────────┘└┘└─────────┘└───────────┘└┘└┘└─┘└┘└─┘└┘└┘└─────┘└─
doc        └────┘           └┘           └───────────┘  └┘   └┘   └┘ └┘       └─
txt        └────┘           └┘           └───────────┘  └┘   └┘   └┘ └┘       └─
par        └────┘           └┘           └───────────┘  └┘   └┘   └┘ └┘       └─
pid                       └┘           └───────────┘  └┘   └┘   └┘ └┘       
st   ───────────────────────────────────────────────────────────────────────────
109    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
110  
111  instance : denumerable code :=
id              └─────────┘ └──┘
src             └─────────┘ └──┘
typ             └─────────┘ └──┘
doc             └─────────┘
112  mk' ⟨encode_code, of_nat_code,
id   └─┘  └─────────┘  └─────────┘
src  └─┘  └─────────┘  └─────────┘
typ  └─┘  └─────────┘  └─────────┘
113    λ c, by induction c; try {refl}; simp [
id                      
src            └────────┘   └───┘└──┘  └──────
typ           └────────┘  └───┘└──┘  └──────
doc            └────────┘   └───┘└──┘  └──────
txt            └────────┘   └───┘└──┘  └──────
par            └────────┘   └───┘└──┘  └──────
pid                           └─────┘      └─
st            └─────────────────┘└──┘└┘└───────
114      encode_code, of_nat_code, -add_comm, *],
id       └─────────┘  └─────────┘
src  ───┘└─────────┘└┘└─────────┘└─────────────┘
typ  ───┘└─────────┘└┘└─────────┘└─────────────┘
doc  ───┘           └┘           └─────────────┘
txt  ───┘           └┘           └─────────────┘
par  ───┘           └┘           └─────────────┘
pid  ───┘           └┘           └─────────────┘
st   ──────────────────────────────────────────┘
115    encode_of_nat_code⟩
id     └────────────────┘
src    └────────────────┘
typ    └────────────────┘
116  
117  theorem encode_code_eq : encode = encode_code := rfl
id                            └────┘  └─────────┘    └─┘
src                           └────┘  └─────────┘    └─┘
typ                           └────┘  └─────────┘    └─┘
118  theorem of_nat_code_eq : of_nat code = of_nat_code := rfl
id                            └────┘ └──┘  └─────────┘    └─┘
src                           └────┘ └──┘  └─────────┘    └─┘
typ                           └────┘ └──┘  └─────────┘    └─┘
119  
120  theorem encode_lt_pair (cf cg) :
121    encode cf < encode (pair cf cg) ∧
id     └────┘ └┘  └────┘  └──┘ └┘ └┘  
src    └────┘     └────┘  └──┘        
typ    └────┘ └┘  └────┘  └──┘ └┘ └┘  
122    encode cg < encode (pair cf cg) :=
id     └────┘ └┘  └────┘  └──┘ └┘ └┘
src    └────┘     └────┘  └──┘
typ    └────┘ └┘  └────┘  └──┘ └┘ └┘
123  begin
st   └─────
124    simp [encode_code_eq, encode_code, -add_comm],
id           └────────────┘  └─────────┘
src    └────┘└────────────┘└┘└─────────┘└──────────┘
typ    └────┘└────────────┘└┘└─────────┘└──────────┘
doc    └────┘              └┘           └──────────┘
txt    └────┘              └┘           └──────────┘
par    └────┘              └┘           └──────────┘
pid                      └┘           └──────────┘
st   ──────────────────────────────────────────────┘└─
125    have := nat.mul_le_mul_right _ (dec_trivial : 1 ≤ 2*2),
id             └──────────────────┘    └─────────┘       
src    └──────┘└──────────────────┘└─┘ └─────────┘└───┘└┘└┘
typ    └──────┘└──────────────────┘└─┘ └─────────┘└───┘└┘└┘
doc    └──────┘                    └─┘ └─────────┘└───┘ └┘ └┘
txt    └──────┘                    └─┘            └───┘ └┘ └┘
par    └──────┘                    └─┘            └───┘ └┘ └┘
pid    └───┘└─┘                    └─┘            └───┘ └┘ └┘
st   ───────────────────────────────────────────────────────┘└─
126    rw [one_mul, mul_assoc, ← bit0_eq_two_mul, ← bit0_eq_two_mul] at this,
id         └─────┘  └───────┘    └─────────────┘    └─────────────┘
src    └──┘└─────┘└┘└───────┘└──┘└─────────────┘└──┘└─────────────┘└───────┘
typ    └──┘└─────┘└┘└───────┘└──┘└─────────────┘└──┘└─────────────┘└───────┘
doc    └──┘       └┘         └──┘               └──┘               └───────┘
txt    └──┘       └┘         └──┘               └──┘               └───────┘
par    └──┘       └┘         └──┘               └──┘               └───────┘
pid      └┘       └┘         └──┘               └──┘               └──────┘
st   ────────────┘└─────────┘└─────────────────┘└─────────────────┘└──────┘└─
127    have := lt_of_le_of_lt this (lt_add_of_pos_right _ (dec_trivial:0<4)),
id             └────────────┘ └──┘  └─────────────────┘                 
src    └──────┘└────────────┘     └─────────────────┘└─┘            └┘└─┘
typ    └──────┘└────────────┘└──┘ └─────────────────┘└─┘            └┘└─┘
doc    └──────┘                                      └─┘            └┘ └─┘
txt    └──────┘                                      └─┘            └┘ └─┘
par    └──────┘                                      └─┘            └┘ └─┘
pid    └───┘└─┘                                      └─┘            └┘ └─┘
st   ──────────────────────────────────────────────────────────────────────┘└─
128    exact ⟨
src    └────┘ 
typ    └────┘ 
doc    └────┘ 
txt    └────┘ 
par    └────┘ 
pid          
st   ──────────
129      lt_of_le_of_lt (nat.le_mkpair_left _ _) this,
id                       └────────────────┘
src  ───┘               └────────────────┘└────┘    └─
typ  ───┘               └────────────────┘└────┘    └─
doc  ───┘                                 └────┘    └─
txt  ───┘                                 └────┘    └─
par  ───┘                                 └────┘    └─
pid  ───┘                                 └────┘    └─
st   ──────────────────────────────────────────────────
130      lt_of_le_of_lt (nat.le_mkpair_right _ _) this⟩
id       └────────────┘  └─────────────────┘      └──┘
src  ───┘└────────────┘ └─────────────────┘└────┘    └┘
typ  ───┘└────────────┘ └─────────────────┘└────┘└──┘└┘
doc  ───┘                                  └────┘    └┘
txt  ───┘                                  └────┘    └┘
par  ───┘                                  └────┘    └┘
pid  ───┘                                  └────┘    
st   ──────────────────────────────────────────────────┘
131  end
st   └─┘
132  
133  theorem encode_lt_comp (cf cg) :
134    encode cf < encode (comp cf cg) ∧
id     └────┘ └┘  └────┘  └──┘ └┘ └┘  
src    └────┘     └────┘  └──┘        
typ    └────┘ └┘  └────┘  └──┘ └┘ └┘  
135    encode cg < encode (comp cf cg) :=
id     └────┘ └┘  └────┘  └──┘ └┘ └┘
src    └────┘     └────┘  └──┘
typ    └────┘ └┘  └────┘  └──┘ └┘ └┘
136  begin
st   └─────
137    suffices, exact (encode_lt_pair cf cg).imp
id                      └────────────┘ └┘ └┘
src    └──────┘  └────┘ └────────────┘    └─────
typ    └──────┘  └────┘ └────────────┘└┘└┘└─────
doc    └──────┘  └────┘                   └─────
txt    └──────┘  └────┘                   └─────
par    └──────┘  └────┘                   └─────
pid    └──────┘                          └─────
st   ─────────┘└──────────────────────────────────
138      (λ h, lt_trans h this) (λ h, lt_trans h this),
id                                    └──────┘   └──┘
src  ───┘  └──┘             └┘  └──┘└──────┘     
typ  ───┘  └──┘             └┘  └──┘└──────┘ └──┘
doc  ───┘  └──┘             └┘  └──┘             
txt  ───┘  └──┘             └┘  └──┘             
par  ───┘  └──┘             └┘  └──┘             
pid  ───┘  └──┘             └┘  └──┘             
st   ────────────────────────────────────────────────┘└─
139    change _, simp [encode_code_eq, encode_code, -add_comm],
id                     └────────────┘  └─────────┘
src    └──────┘  └────┘└────────────┘└┘└─────────┘└──────────┘
typ    └──────┘  └────┘└────────────┘└┘└─────────┘└──────────┘
doc    └──────┘  └────┘              └┘           └──────────┘
txt    └──────┘  └────┘              └┘           └──────────┘
par    └──────┘  └────┘              └┘           └──────────┘
pid          └┘                    └┘           └──────────┘
st   ────────────────────────────────────────────────────────┘└─
140    exact nat.bit0_lt (nat.lt_succ_self _),
id           └─────────┘  └──────────────┘
src    └────┘└─────────┘ └──────────────┘└─┘
typ    └────┘└─────────┘ └──────────────┘└─┘
doc    └────┘                            └─┘
txt    └────┘                            └─┘
par    └────┘                            └─┘
pid                                     └─┘
st   ───────────────────────────────────────┘└─
141  end
st   ──┘
142  
143  theorem encode_lt_prec (cf cg) :
144    encode cf < encode (prec cf cg) ∧
id     └────┘ └┘  └────┘  └──┘ └┘ └┘  
src    └────┘     └────┘  └──┘        
typ    └────┘ └┘  └────┘  └──┘ └┘ └┘  
145    encode cg < encode (prec cf cg) :=
id     └────┘ └┘  └────┘  └──┘ └┘ └┘
src    └────┘     └────┘  └──┘
typ    └────┘ └┘  └────┘  └──┘ └┘ └┘
146  begin
st   └─────
147    suffices, exact (encode_lt_pair cf cg).imp
id                      └────────────┘ └┘ └┘
src    └──────┘  └────┘ └────────────┘    └─────
typ    └──────┘  └────┘ └────────────┘└┘└┘└─────
doc    └──────┘  └────┘                   └─────
txt    └──────┘  └────┘                   └─────
par    └──────┘  └────┘                   └─────
pid    └──────┘                          └─────
st   ─────────┘└──────────────────────────────────
148      (λ h, lt_trans h this) (λ h, lt_trans h this),
id                                    └──────┘   └──┘
src  ───┘  └──┘             └┘  └──┘└──────┘     
typ  ───┘  └──┘             └┘  └──┘└──────┘ └──┘
doc  ───┘  └──┘             └┘  └──┘             
txt  ───┘  └──┘             └┘  └──┘             
par  ───┘  └──┘             └┘  └──┘             
pid  ───┘  └──┘             └┘  └──┘             
st   ────────────────────────────────────────────────┘└─
149    change _, simp [encode_code_eq, encode_code, -add_comm],
id                     └────────────┘  └─────────┘
src    └──────┘  └────┘└────────────┘└┘└─────────┘└──────────┘
typ    └──────┘  └────┘└────────────┘└┘└─────────┘└──────────┘
doc    └──────┘  └────┘              └┘           └──────────┘
txt    └──────┘  └────┘              └┘           └──────────┘
par    └──────┘  └────┘              └┘           └──────────┘
pid          └┘                    └┘           └──────────┘
st   ────────────────────────────────────────────────────────┘└─
150    exact nat.lt_succ_self _,
id           └──────────────┘
src    └────┘└──────────────┘└┘
typ    └────┘└──────────────┘└┘
doc    └────┘                └┘
txt    └────┘                └┘
par    └────┘                └┘
pid                         └┘
st   ─────────────────────────┘└─
151  end
st   ──┘
152  
153  theorem encode_lt_rfind' (cf) : encode cf < encode (rfind' cf) :=
id                                   └────┘ └┘  └────┘  └────┘ └┘
src                                  └────┘     └────┘  └────┘
typ                                  └────┘ └┘  └────┘  └────┘ └┘
154  begin
st   └─────
155    simp [encode_code_eq, encode_code, -add_comm],
id           └────────────┘  └─────────┘
src    └────┘└────────────┘└┘└─────────┘└──────────┘
typ    └────┘└────────────┘└┘└─────────┘└──────────┘
doc    └────┘              └┘           └──────────┘
txt    └────┘              └┘           └──────────┘
par    └────┘              └┘           └──────────┘
pid                      └┘           └──────────┘
st   ──────────────────────────────────────────────┘└─
156    have := nat.mul_le_mul_right _ (dec_trivial : 1 ≤ 2*2),
id             └──────────────────┘    └─────────┘       
src    └──────┘└──────────────────┘└─┘ └─────────┘└───┘└┘└┘
typ    └──────┘└──────────────────┘└─┘ └─────────┘└───┘└┘└┘
doc    └──────┘                    └─┘ └─────────┘└───┘ └┘ └┘
txt    └──────┘                    └─┘            └───┘ └┘ └┘
par    └──────┘                    └─┘            └───┘ └┘ └┘
pid    └───┘└─┘                    └─┘            └───┘ └┘ └┘
st   ───────────────────────────────────────────────────────┘└─
157    rw [one_mul, mul_assoc, ← bit0_eq_two_mul, ← bit0_eq_two_mul] at this,
id         └─────┘  └───────┘    └─────────────┘    └─────────────┘
src    └──┘└─────┘└┘└───────┘└──┘└─────────────┘└──┘└─────────────┘└───────┘
typ    └──┘└─────┘└┘└───────┘└──┘└─────────────┘└──┘└─────────────┘└───────┘
doc    └──┘       └┘         └──┘               └──┘               └───────┘
txt    └──┘       └┘         └──┘               └──┘               └───────┘
par    └──┘       └┘         └──┘               └──┘               └───────┘
pid      └┘       └┘         └──┘               └──┘               └──────┘
st   ────────────┘└─────────┘└─────────────────┘└─────────────────┘└──────┘└─
158    refine lt_of_le_of_lt (le_trans this _)
id            └────────────┘  └──────┘ └──┘
src    └─────┘└────────────┘ └──────┘    └───
typ    └─────┘└────────────┘ └──────┘└──┘└───
doc    └─────┘                           └───
txt    └─────┘                           └───
par    └─────┘                           └───
pid                                     └───
st   ──────────────────────────────────────────
159      (lt_add_of_pos_right _ (dec_trivial:0<4)),
id        └─────────────────┘                 
src  ───┘ └─────────────────┘└─┘            └┘└─┘
typ  ───┘ └─────────────────┘└─┘            └┘└─┘
doc  ───┘                    └─┘            └┘ └─┘
txt  ───┘                    └─┘            └┘ └─┘
par  ───┘                    └─┘            └┘ └─┘
pid  ───┘                    └─┘            └┘ └─┘
st   ────────────────────────────────────────────┘└─
160    exact le_of_lt (nat.bit0_lt_bit1 $ le_of_lt $
id                                        └──────┘
src    └────┘                          └──────┘ 
typ    └────┘                          └──────┘ 
doc    └────┘                                   
txt    └────┘                                   
par    └────┘                                   
pid                                            
st   ────────────────────────────────────────────────
161      nat.bit0_lt_bit1 $ le_refl _),
id       └──────────────┘   └─────┘
src  ───┘└──────────────┘ └─────┘└─┘
typ  ───┘└──────────────┘ └─────┘└─┘
doc  ───┘                        └─┘
txt  ───┘                        └─┘
par  ───┘                        └─┘
pid  ───┘                        └─┘
st   ────────────────────────────────┘└─
162  end
st   ──┘
163  
164  section
165  open primrec
166  
167  theorem pair_prim : primrec₂ pair :=
id                       └──────┘ └──┘
src                      └──────┘ └──┘
typ                      └──────┘ └──┘
doc                      └──────┘
168  primrec₂.of_nat_iff.2 $ primrec₂.encode_iff.1 $ nat_add.comp
id   └─────────────────┘    └─────────────────┘    └─────┘└───┘
src  └─────────────────┘    └─────────────────┘    └─────┘└───┘
typ  └─────────────────┘    └─────────────────┘    └─────┘└───┘
169    (nat_bit0.comp $ nat_bit0.comp $
id      └──────┘└───┘   └──────┘└───┘
src     └──────┘└───┘   └──────┘└───┘
typ     └──────┘└───┘   └──────┘└───┘
170      primrec₂.mkpair.comp
id       └─────────────┘└───┘
src      └─────────────┘└───┘
typ      └─────────────┘└───┘
171        (encode_iff.2 $ (primrec.of_nat code).comp fst)
id          └────────┘     └────────────┘ └──┘ └──┘  └─┘
src         └────────┘     └────────────┘ └──┘ └──┘  └─┘
typ         └────────┘     └────────────┘ └──┘ └──┘  └─┘
172        (encode_iff.2 $ (primrec.of_nat code).comp snd))
id          └────────┘     └────────────┘ └──┘ └──┘  └─┘
src         └────────┘     └────────────┘ └──┘ └──┘  └─┘
typ         └────────┘     └────────────┘ └──┘ └──┘  └─┘
173    (primrec₂.const 4)
id      └────────────┘
src     └────────────┘
typ     └────────────┘
174  
175  theorem comp_prim : primrec₂ comp :=
id                       └──────┘ └──┘
src                      └──────┘ └──┘
typ                      └──────┘ └──┘
doc                      └──────┘
176  primrec₂.of_nat_iff.2 $ primrec₂.encode_iff.1 $ nat_add.comp
id   └─────────────────┘    └─────────────────┘    └─────┘└───┘
src  └─────────────────┘    └─────────────────┘    └─────┘└───┘
typ  └─────────────────┘    └─────────────────┘    └─────┘└───┘
177    (nat_bit0.comp $ nat_bit1.comp $
id      └──────┘└───┘   └──────┘└───┘
src     └──────┘└───┘   └──────┘└───┘
typ     └──────┘└───┘   └──────┘└───┘
178      primrec₂.mkpair.comp
id       └─────────────┘└───┘
src      └─────────────┘└───┘
typ      └─────────────┘└───┘
179        (encode_iff.2 $ (primrec.of_nat code).comp fst)
id          └────────┘     └────────────┘ └──┘ └──┘  └─┘
src         └────────┘     └────────────┘ └──┘ └──┘  └─┘
typ         └────────┘     └────────────┘ └──┘ └──┘  └─┘
180        (encode_iff.2 $ (primrec.of_nat code).comp snd))
id          └────────┘     └────────────┘ └──┘ └──┘  └─┘
src         └────────┘     └────────────┘ └──┘ └──┘  └─┘
typ         └────────┘     └────────────┘ └──┘ └──┘  └─┘
181    (primrec₂.const 4)
id      └────────────┘
src     └────────────┘
typ     └────────────┘
182  
183  theorem prec_prim : primrec₂ prec :=
id                       └──────┘ └──┘
src                      └──────┘ └──┘
typ                      └──────┘ └──┘
doc                      └──────┘
184  primrec₂.of_nat_iff.2 $ primrec₂.encode_iff.1 $ nat_add.comp
id   └─────────────────┘    └─────────────────┘    └─────┘└───┘
src  └─────────────────┘    └─────────────────┘    └─────┘└───┘
typ  └─────────────────┘    └─────────────────┘    └─────┘└───┘
185    (nat_bit1.comp $ nat_bit0.comp $
id      └──────┘└───┘   └──────┘└───┘
src     └──────┘└───┘   └──────┘└───┘
typ     └──────┘└───┘   └──────┘└───┘
186      primrec₂.mkpair.comp
id       └─────────────┘└───┘
src      └─────────────┘└───┘
typ      └─────────────┘└───┘
187        (encode_iff.2 $ (primrec.of_nat code).comp fst)
id          └────────┘     └────────────┘ └──┘ └──┘  └─┘
src         └────────┘     └────────────┘ └──┘ └──┘  └─┘
typ         └────────┘     └────────────┘ └──┘ └──┘  └─┘
188        (encode_iff.2 $ (primrec.of_nat code).comp snd))
id          └────────┘     └────────────┘ └──┘ └──┘  └─┘
src         └────────┘     └────────────┘ └──┘ └──┘  └─┘
typ         └────────┘     └────────────┘ └──┘ └──┘  └─┘
189    (primrec₂.const 4)
id      └────────────┘
src     └────────────┘
typ     └────────────┘
190  
191  theorem rfind_prim : primrec rfind' :=
id                        └─────┘ └────┘
src                       └─────┘ └────┘
typ                       └─────┘ └────┘
doc                       └─────┘
192  of_nat_iff.2 $ encode_iff.1 $ nat_add.comp
id   └────────┘    └────────┘    └─────┘└───┘
src  └────────┘    └────────┘    └─────┘└───┘
typ  └────────┘    └────────┘    └─────┘└───┘
193    (nat_bit1.comp $ nat_bit1.comp $
id      └──────┘└───┘   └──────┘└───┘
src     └──────┘└───┘   └──────┘└───┘
typ     └──────┘└───┘   └──────┘└───┘
194      encode_iff.2 $ primrec.of_nat code)
id       └────────┘    └────────────┘ └──┘
src      └────────┘    └────────────┘ └──┘
typ      └────────┘    └────────────┘ └──┘
195    (const 4)
id      └───┘
src     └───┘
typ     └───┘
196  
197  theorem rec_prim' {α σ} [primcodable α] [primcodable σ]
id                            └─────────┘    └─────────┘ 
src                           └─────────┘     └─────────┘
typ                           └─────────┘    └─────────┘ 
doc                           └─────────┘     └─────────┘
198    {c : α → code} (hc : primrec c)
id             └──┘        └─────┘ 
src             └──┘        └─────┘
typ            └──┘        └─────┘ 
doc                         └─────┘
199    {z : α → σ} (hz : primrec z)
id                     └─────┘ 
src                      └─────┘
typ                    └─────┘ 
doc                      └─────┘
200    {s : α → σ} (hs : primrec s)
id                     └─────┘ 
src                      └─────┘
typ                    └─────┘ 
doc                      └─────┘
201    {l : α → σ} (hl : primrec l)
id                     └─────┘ 
src                      └─────┘
typ                    └─────┘ 
doc                      └─────┘
202    {r : α → σ} (hr : primrec r)
id                     └─────┘ 
src                      └─────┘
typ                    └─────┘ 
doc                      └─────┘
203    {pr : α → code × code × σ × σ → σ} (hpr : primrec₂ pr)
id              └──┘  └──┘                └──────┘ └┘
src              └──┘  └──┘                   └──────┘
typ             └──┘  └──┘                └──────┘ └┘
doc                                              └──────┘
204    {co : α → code × code × σ × σ → σ} (hco : primrec₂ co)
id              └──┘  └──┘                └──────┘ └┘
src              └──┘  └──┘                   └──────┘
typ             └──┘  └──┘                └──────┘ └┘
doc                                              └──────┘
205    {pc : α → code × code × σ × σ → σ} (hpc : primrec₂ pc)
id              └──┘  └──┘                └──────┘ └┘
src              └──┘  └──┘                   └──────┘
typ             └──┘  └──┘                └──────┘ └┘
doc                                              └──────┘
206    {rf : α → code × σ → σ} (hrf : primrec₂ rf) :
id              └──┘              └──────┘ └┘
src              └──┘                └──────┘
typ             └──┘              └──────┘ └┘
doc                                   └──────┘
207  let PR (a) := λ cf cg hf hg, pr a (cf, cg, hf, hg),
id       └┘         └┘ └┘ └┘ └┘  └┘  └┘  └┘  └┘  └┘
src                                    
typ      └┘         └┘ └┘ └┘ └┘  └┘  └┘  └┘  └┘  └┘
208      CO (a) := λ cf cg hf hg, co a (cf, cg, hf, hg),
id       └┘         └┘ └┘ └┘ └┘  └┘  └┘  └┘  └┘  └┘
src                                    
typ      └┘         └┘ └┘ └┘ └┘  └┘  └┘  └┘  └┘  └┘
209      PC (a) := λ cf cg hf hg, pc a (cf, cg, hf, hg),
id       └┘         └┘ └┘ └┘ └┘  └┘  └┘  └┘  └┘  └┘
src                                    
typ      └┘         └┘ └┘ └┘ └┘  └┘  └┘  └┘  └┘  └┘
210      RF (a) := λ cf hf, rf a (cf, hf),
id       └┘         └┘ └┘  └┘  └┘  └┘
src                              
typ      └┘         └┘ └┘  └┘  └┘  └┘
211      F (a c) : σ := nat.partrec.code.rec_on c
id                   └─────────────────────┘ 
src                     └─────────────────────┘
typ                  └─────────────────────┘ 
212        (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a) in
id                          └┘    └┘    └┘    └┘ 
typ                         └┘    └┘    └┘    └┘ 
213      primrec (λ a, F a (c a)) :=
id       └─────┘          
src      └─────┘
typ      └─────┘          
doc      └─────┘
214  begin
st   └─────
215    intros,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ───────┘└─
216    let G₁ : (α × list σ) × ℕ × ℕ → option σ := λ p,
id                 └──┘             └────┘ 
src    └───────┘  └──┘ └┘     └────┘ └──┘ └───
typ    └───────┘ └──┘ └┘    └────┘└──┘ └───
doc    └───────┘        └┘            └──┘ └───
txt    └───────┘        └┘            └──┘ └───
par    └───────┘        └┘            └──┘ └───
pid    └────┘└─┘        └┘            └──┘ └───
st   ───────────────────────────────────────────────────
217      let a := p.1.1, IH := p.1.2, n := p.2.1, m := p.2.2 in
src  ───┘   └────┘ └──────────┘ └─────────┘ └─────────┘ └───────
typ  ───┘   └────┘ └──────────┘ └─────────┘ └─────────┘ └───────
doc  ───┘   └────┘ └──────────┘ └─────────┘ └─────────┘ └───────
txt  ───┘   └────┘ └──────────┘ └─────────┘ └─────────┘ └───────
par  ───┘   └────┘ └──────────┘ └─────────┘ └─────────┘ └───────
pid  ───┘   └────┘ └──────────┘ └─────────┘ └─────────┘ └───────
st   ───────────────────────────────────────────────────────────
218      (IH.nth m).bind $ λ s,
id          └──┘
src  ───┘   └──┘ └─────┘  └───
typ  ───┘   └──┘ └─────┘  └───
doc  ───┘        └─────┘  └───
txt  ───┘        └─────┘  └───
par  ───┘        └─────┘  └───
pid  ───┘        └─────┘  └───
st   ───────────────────────────
219      (IH.nth m.unpair.1).bind $ λ s₁,
id          └──┘  └─────┘
src  ───┘   └──┘ └─────┘└───────┘  └────
typ  ───┘   └──┘ └─────┘└───────┘  └────
doc  ───┘        └─────┘└───────┘  └────
txt  ───┘               └───────┘  └────
par  ───┘               └───────┘  └────
pid  ───┘               └───────┘  └────
st   ─────────────────────────────────────
220      (IH.nth m.unpair.2).map $ λ s₂,
id          └──┘  └─────┘
src  ───┘   └──┘ └─────┘└──────┘  └────
typ  ───┘   └──┘ └─────┘└──────┘  └────
doc  ───┘        └─────┘└──────┘  └────
txt  ───┘               └──────┘  └────
par  ───┘               └──────┘  └────
pid  ───┘               └──────┘  └────
st   ────────────────────────────────────
221      cond n.bodd
id             └───┘
src  ───┘     └───┘
typ  ───┘     └───┘
doc  ───┘          
txt  ───┘          
par  ───┘          
pid  ───┘          
st   ────────────────
222        (cond n.div2.bodd
id                └───┘└───┘
src  ─────┘      └───┘└───┘
typ  ─────┘      └───┘└───┘
doc  ─────┘                
txt  ─────┘                
par  ─────┘                
pid  ─────┘                
st   ────────────────────────
223          (rf a (of_nat code m, s))
id            └┘
src  ───────┘                └┘ └──
typ  ───────┘ └┘             └┘ └──
doc  ───────┘                └┘ └──
txt  ───────┘                └┘ └──
par  ───────┘                └┘ └──
pid  ───────┘                └┘ └──
st   ──────────────────────────────────
224          (pc a (of_nat code m.unpair.1, of_nat code m.unpair.2, s₁, s₂)))
id            └┘                 └─────┘
src  ───────┘                └─────┘└──┘                  └──┘  └┘  └───
typ  ───────┘ └┘             └─────┘└──┘                  └──┘  └┘  └───
doc  ───────┘                └─────┘└──┘                  └──┘  └┘  └───
txt  ───────┘                       └──┘                  └──┘  └┘  └───
par  ───────┘                       └──┘                  └──┘  └┘  └───
pid  ───────┘                       └──┘                  └──┘  └┘  └───
st   ─────────────────────────────────────────────────────────────────────────
225        (cond n.div2.bodd
id          └──┘
src  ─────┘ └──┘           
typ  ─────┘ └──┘           
doc  ─────┘                
txt  ─────┘                
par  ─────┘                
pid  ─────┘                
st   ────────────────────────
226          (co a (of_nat code m.unpair.1, of_nat code m.unpair.2, s₁, s₂))
id            └┘
src  ───────┘                       └──┘                  └──┘  └┘  └──
typ  ───────┘ └┘                    └──┘                  └──┘  └┘  └──
doc  ───────┘                       └──┘                  └──┘  └┘  └──
txt  ───────┘                       └──┘                  └──┘  └┘  └──
par  ───────┘                       └──┘                  └──┘  └┘  └──
pid  ───────┘                       └──┘                  └──┘  └┘  └──
st   ────────────────────────────────────────────────────────────────────────
227          (pr a (of_nat code m.unpair.1, of_nat code m.unpair.2, s₁, s₂))),
id            └┘                            └────┘ └──┘
src  ───────┘                       └──┘└────┘└──┘        └──┘  └┘  └─┘
typ  ───────┘ └┘                    └──┘└────┘└──┘        └──┘  └┘  └─┘
doc  ───────┘                       └──┘                  └──┘  └┘  └─┘
txt  ───────┘                       └──┘                  └──┘  └┘  └─┘
par  ───────┘                       └──┘                  └──┘  └┘  └─┘
pid  ───────┘                       └──┘                  └──┘  └┘  └─┘
st   ───────────────────────────────────────────────────────────────────────┘└─
228    have : primrec G₁,
id            └─────┘ └┘
src    └─────┘└─────┘
typ    └─────┘└─────┘└┘
doc    └─────┘└─────┘
txt    └─────┘       
par    └─────┘       
pid    └───┘└┘       
st   ──────────────────┘└─
229    { refine option_bind (list_nth.comp (snd.comp fst) (snd.comp snd)) _,
id              └─────────┘  └───────────┘           └─┘   └──────┘ └─┘
src      └─────┘└─────────┘ └───────────┘         └─┘└┘ └──────┘└─┘└──┘
typ      └─────┘└─────────┘ └───────────┘         └─┘└┘ └──────┘└─┘└──┘
doc      └─────┘                                     └┘            └──┘
txt      └─────┘                                     └┘            └──┘
par      └─────┘                                     └┘            └──┘
pid                                                 └┘            └──┘
st   ───┘└────────────────────────────────────────────────────────────────┘└─
230      refine option_bind ((list_nth.comp (snd.comp fst)
id              └─────────┘   └───────────┘
src      └─────┘└─────────┘  └───────────┘            └─
typ      └─────┘└─────────┘  └───────────┘            └─
doc      └─────┘                                      └─
txt      └─────┘                                      └─
par      └─────┘                                      └─
pid                                                  └─
st   ──────────────────────────────────────────────────────
231        (fst.comp $ primrec.unpair.comp (snd.comp snd))).comp fst) _,
id          └──────┘   └─────────────────┘  └──────┘ └─┘         └─┘
src  ─────┘ └──────┘ └─────────────────┘ └──────┘└─┘└───────┘└─┘└─┘
typ  ─────┘ └──────┘ └─────────────────┘ └──────┘└─┘└───────┘└─┘└─┘
doc  ─────┘                                         └───────┘   └─┘
txt  ─────┘                                         └───────┘   └─┘
par  ─────┘                                         └───────┘   └─┘
pid  ─────┘                                         └───────┘   └─┘
st   ─────────────────────────────────────────────────────────────────┘└─
232      refine option_map ((list_nth.comp (snd.comp fst)
id              └────────┘   └───────────┘
src      └─────┘└────────┘  └───────────┘            └─
typ      └─────┘└────────┘  └───────────┘            └─
doc      └─────┘                                     └─
txt      └─────┘                                     └─
par      └─────┘                                     └─
pid                                                 └─
st   ─────────────────────────────────────────────────────
233        (snd.comp $ primrec.unpair.comp (snd.comp snd))).comp $ fst.comp fst) _,
id                     └─────────────────┘  └──────┘ └─┘           └──────┘ └─┘
src  ─────┘          └─────────────────┘ └──────┘└─┘└───────┘ └──────┘└─┘└─┘
typ  ─────┘          └─────────────────┘ └──────┘└─┘└───────┘ └──────┘└─┘└─┘
doc  ─────┘                                         └───────┘            └─┘
txt  ─────┘                                         └───────┘            └─┘
par  ─────┘                                         └───────┘            └─┘
pid  ─────┘                                         └───────┘            └─┘
st   ────────────────────────────────────────────────────────────────────────────┘└─
234      have a := fst.comp (fst.comp $ fst.comp $ fst.comp fst),
id                                                 └──────┘ └─┘
src      └────────┘                           └──────┘└─┘
typ      └────────┘                           └──────┘└─┘
doc      └────────┘                                      
txt      └────────┘                                      
par      └────────┘                                      
pid      └────┘└─┘                                      
st   ──────────────────────────────────────────────────────────┘└─
235      have n := fst.comp (snd.comp $ fst.comp $ fst.comp fst),
id                           └──────┘              └──────┘ └─┘
src      └────────┘         └──────┘          └──────┘└─┘
typ      └────────┘         └──────┘          └──────┘└─┘
doc      └────────┘                                      
txt      └────────┘                                      
par      └────────┘                                      
pid      └────┘└─┘                                      
st   ──────────────────────────────────────────────────────────┘└─
236      have m := snd.comp (snd.comp $ fst.comp $ fst.comp fst),
id                           └──────┘              └──────┘ └─┘
src      └────────┘         └──────┘          └──────┘└─┘
typ      └────────┘         └──────┘          └──────┘└─┘
doc      └────────┘                                      
txt      └────────┘                                      
par      └────────┘                                      
pid      └────┘└─┘                                      
st   ──────────────────────────────────────────────────────────┘└─
237      have m₁ := fst.comp (primrec.unpair.comp m),
id                  └──────┘  └─────────────────┘ 
src      └─────────┘└──────┘ └─────────────────┘ 
typ      └─────────┘└──────┘ └─────────────────┘
doc      └─────────┘                             
txt      └─────────┘                             
par      └─────────┘                             
pid      └─────┘└─┘                             
st   ──────────────────────────────────────────────┘└─
238      have m₂ := snd.comp (primrec.unpair.comp m),
id                  └──────┘  └─────────────────┘ 
src      └─────────┘└──────┘ └─────────────────┘ 
typ      └─────────┘└──────┘ └─────────────────┘
doc      └─────────┘                             
txt      └─────────┘                             
par      └─────────┘                             
pid      └─────┘└─┘                             
st   ──────────────────────────────────────────────┘└─
239      have s := snd.comp (fst.comp fst),
id                 └──────┘  └──────┘ └─┘
src      └────────┘└──────┘ └──────┘└─┘
typ      └────────┘└──────┘ └──────┘└─┘
doc      └────────┘                    
txt      └────────┘                    
par      └────────┘                    
pid      └────┘└─┘                    
st   ────────────────────────────────────┘└─
240      have s₁ := snd.comp fst,
id                  └──────┘ └─┘
src      └─────────┘└──────┘└─┘
typ      └─────────┘└──────┘└─┘
doc      └─────────┘        
txt      └─────────┘        
par      └─────────┘        
pid      └─────┘└─┘        
st   ──────────────────────────┘
241      have s₂ := snd,
242      exact (nat_bodd.comp n).cond
243        ((nat_bodd.comp $ nat_div2.comp n).cond
244          (hrf.comp a (((primrec.of_nat code).comp m).pair s))
245          (hpc.comp a (((primrec.of_nat code).comp m₁).pair $
246            ((primrec.of_nat code).comp m₂).pair $ s₁.pair s₂)))
247        (primrec.cond (nat_bodd.comp $ nat_div2.comp n)
248          (hco.comp a (((primrec.of_nat code).comp m₁).pair $
249            ((primrec.of_nat code).comp m₂).pair $ s₁.pair s₂))
250          (hpr.comp a (((primrec.of_nat code).comp m₁).pair $
251            ((primrec.of_nat code).comp m₂).pair $ s₁.pair s₂))) },
id                              └──┘
src                             └──┘
typ                             └──┘
st                                                                  └┘
252    let G : α → list σ → option σ := λ a IH,
id                └──┘     └────┘        └┘
src                └──┘     └────┘
typ               └──┘     └────┘        └┘
253      IH.length.cases (some (z a)) $ λ n,
id                                       
typ                                      
254      n.cases (some (s a)) $ λ n,
id                               
typ                              
255      n.cases (some (l a)) $ λ n,
id                               
typ                              
256      n.cases (some (r a)) $ λ n,
id                               
typ                              
257      G₁ ((a, IH), n, n.div2.div2),
id                        └────────┘
src                       └────────┘
typ                       └────────┘
258    have : primrec₂ G := (nat_cases
259      (list_length.comp snd) (option_some_iff.2 (hz.comp fst)) $
260      nat_cases snd (option_some_iff.2 (hs.comp (fst.comp fst))) $
261      nat_cases snd (option_some_iff.2 (hl.comp (fst.comp $ fst.comp fst))) $
262      nat_cases snd (option_some_iff.2 (hr.comp (fst.comp $ fst.comp $ fst.comp fst)))
263      (this.comp $
264        ((fst.pair snd).comp $ fst.comp $ fst.comp $ fst.comp $ fst).pair $
265        snd.pair $ nat_div2.comp $ nat_div2.comp snd)),
266    refine ((nat_strong_rec
267      (λ a n, F a (of_nat code n)) this.to₂ $ λ a n, _).comp
id                        └──┘                   
src                          └──┘
typ                       └──┘                   
268      primrec.id $ encode_iff.2 hc).of_eq (λ a, by simp),
id                                              
typ                                             
269    simp,
270    iterate 4 {cases n with n, {refl}},
id                      
typ                     
st                                     
271    simp [G], rw [list.length_map, list.length_range],
272    let m := n.div2.div2,
id              └─────────┘
src             └─────────┘
typ             └─────────┘
273    show G₁ ((a, (list.range (n+4)).map (λ n, F a (of_nat code n))), n, m)
id                   └────────┘                                           
src                  └────────┘
typ                  └────────┘                                           
274      = some (F a (of_nat code (n+4))),
id                          └──┘  
src                          └──┘
typ                         └──┘  
275    have hm : m < n + 4, by simp [nat.div2_val, m];
id                                               
typ                                              
276    from lt_of_le_of_lt
277      (le_trans (nat.div_le_self _ _) (nat.div_le_self _ _))
278      (nat.succ_le_succ (nat.le_add_right _ _)),
279    have m1 : m.unpair.1 < n + 4, from lt_of_le_of_lt m.unpair_le_left hm,
id               └──────┘     
src              └──────┘
typ              └──────┘     
doc              └──────┘
280    have m2 : m.unpair.2 < n + 4, from lt_of_le_of_lt m.unpair_le_right hm,
id               └──────┘     
src              └──────┘
typ              └──────┘     
doc              └──────┘
281    simp [G₁], simp [list.nth_map, list.nth_range, hm, m1, m2],
282    change of_nat code (n+4) with of_nat_code (n+4),
id                   └──┘           └─────────┘  
src                  └──┘            └─────────┘
typ                  └──┘           └─────────┘  
283    simp [of_nat_code],
id           └─────────┘
src          └─────────┘
typ          └─────────┘
284    cases n.bodd; cases n.div2.bodd; refl
id           └────┘                     └──┘
src          └────┘                     └──┘
typ          └────┘                     └──┘
doc                                     └──┘
285  end
st   └─┘
286  
287  theorem rec_prim {α σ} [primcodable α] [primcodable σ]
id                           └──┘  └──┘      └┘ └┘ └┘  
src                          └──┘  └──┘       └┘ └┘ └┘
typ                          └──┘  └──┘      └┘ └┘ └┘  
doc                          └──┘  └──┘       └┘ └┘ └┘
288    {c : α → code} (hc : primrec c)
id             └──┘                
src             └──┘
typ            └──┘                
289    {z : α → σ} (hz : primrec z)
id                             
typ                            
290    {s : α → σ} (hs : primrec s)
id                             
typ                            
291    {l : α → σ} (hl : primrec l)
id                              
typ                             
292    {r : α → σ} (hr : primrec r)
id                             
typ                            
293    {pr : α → code → code → σ → σ → σ}
id              └──┘   └──┘         
src              └──┘   └──┘
typ             └──┘   └──┘         
294    (hpr : primrec (λ a : α × code × code × σ × σ,
id                              └──┘   └──┘      
src                              └──┘   └──┘
typ                             └──┘   └──┘      
295      pr a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2))
296    {co : α → code → code → σ → σ → σ}
id              └──┘   └──┘         
src              └──┘   └──┘
typ             └──┘   └──┘         
297    (hco : primrec (λ a : α × code × code × σ × σ,
id                              └──┘  └──┘     
src                              └──┘  └──┘ 
typ                             └──┘  └──┘     
298      co a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2))
299    {pc : α → code → code → σ → σ → σ}
id                                 
src                      
typ                                
300    (hpc : primrec (λ a : α × code × code × σ × σ,
id                              └──┘  └──┘    
src                              └──┘  └──┘    
typ                             └──┘  └──┘    
301      pc a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2))
302    {rf : α → code → σ → σ}
id              └──┘      
src              └──┘
typ             └──┘      
303    (hrf : primrec (λ a : α × code × σ, rf a.1 a.2.1 a.2.2)) :
id                              └──┘    └┘
src                              └──┘ 
typ                             └──┘    └┘
304  let F (a c) : σ := nat.partrec.code.rec_on c
id                                           
typ                                          
305        (z a) (s a) (l a) (r a) (pr a) (co a) (pc a) (rf a) in
id                                            └┘ 
typ                                           └┘ 
306      primrec (λ a, F a (c a)) :=
id                        
typ                       
307  begin
308    intros,
309    let G₁ : (α × list σ) × ℕ × ℕ → option σ := λ p,
id                  └──┘              └────┘ 
src                  └──┘              └────┘
typ                 └──┘              └────┘ 
310      let a := p.1.1, IH := p.1.2, n := p.2.1, m := p.2.2 in
id                      └┘                      
typ                     └┘                      
311      (IH.nth m).bind $ λ s,
id                           
typ                          
312      (IH.nth m.unpair.1).bind $ λ s₁,
id                └─────┘             └┘
src               └─────┘
typ               └─────┘             └┘
doc               └─────┘
313      (IH.nth m.unpair.2).map $ λ s₂,
id                └─────┘            └┘
src               └─────┘
typ               └─────┘            └┘
doc               └─────┘
314      cond n.bodd
id             └───┘
src            └───┘
typ            └───┘
315        (cond n.div2.bodd
id                └───┘└───┘
src               └───┘└───┘
typ               └───┘└───┘
316          (rf a (of_nat code m) s)
id            └┘
typ           └┘
317          (pc a (of_nat code m.unpair.1) (of_nat code m.unpair.2) s₁ s₂))
318        (cond n.div2.bodd
319          (co a (of_nat code m.unpair.1) (of_nat code m.unpair.2) s₁ s₂)
320          (pr a (of_nat code m.unpair.1) (of_nat code m.unpair.2) s₁ s₂)),
id                                                  └──┘
src                                                 └──┘
typ                                                 └──┘
321    have : primrec G₁,
322    { refine option_bind (list_nth.comp (snd.comp fst) (snd.comp snd)) _,
323      refine option_bind ((list_nth.comp (snd.comp fst)
324        (fst.comp $ primrec.unpair.comp (snd.comp snd))).comp fst) _,
325      refine option_map ((list_nth.comp (snd.comp fst)
326        (snd.comp $ primrec.unpair.comp (snd.comp snd))).comp $ fst.comp fst) _,
327      have a := fst.comp (fst.comp $ fst.comp $ fst.comp fst),
328      have n := fst.comp (snd.comp $ fst.comp $ fst.comp fst),
329      have m := snd.comp (snd.comp $ fst.comp $ fst.comp fst),
330      have m₁ := fst.comp (primrec.unpair.comp m),
331      have m₂ := snd.comp (primrec.unpair.comp m),
332      have s := snd.comp (fst.comp fst),
333      have s₁ := snd.comp fst,
334      have s₂ := snd,
335      exact (nat_bodd.comp n).cond
336        ((nat_bodd.comp $ nat_div2.comp n).cond
337          (hrf.comp $ a.pair (((primrec.of_nat code).comp m).pair s))
338          (hpc.comp $ a.pair (((primrec.of_nat code).comp m₁).pair $
339            ((primrec.of_nat code).comp m₂).pair $ s₁.pair s₂)))
340        (primrec.cond (nat_bodd.comp $ nat_div2.comp n)
341          (hco.comp $ a.pair (((primrec.of_nat code).comp m₁).pair $
342            ((primrec.of_nat code).comp m₂).pair $ s₁.pair s₂))
343          (hpr.comp $ a.pair (((primrec.of_nat code).comp m₁).pair $
344            ((primrec.of_nat code).comp m₂).pair $ s₁.pair s₂))) },
id                              └──┘
src                             └──┘
typ                             └──┘
st                                                                  └┘
345    let G : α → list σ → option σ := λ a IH,
id                └──┘     └────┘        └┘
src                └──┘     └────┘
typ               └──┘     └────┘        └┘
346      IH.length.cases (some (z a)) $ λ n,
id                                       
typ                                      
347      n.cases (some (s a)) $ λ n,
id                               
typ                              
348      n.cases (some (l a)) $ λ n,
id                               
typ                              
349      n.cases (some (r a)) $ λ n,
id                               
typ                              
350      G₁ ((a, IH), n, n.div2.div2),
id                        └────────┘
src                       └────────┘
typ                       └────────┘
351    have : primrec₂ G := (nat_cases
352      (list_length.comp snd) (option_some_iff.2 (hz.comp fst)) $
353      nat_cases snd (option_some_iff.2 (hs.comp (fst.comp fst))) $
354      nat_cases snd (option_some_iff.2 (hl.comp (fst.comp $ fst.comp fst))) $
355      nat_cases snd (option_some_iff.2 (hr.comp (fst.comp $ fst.comp $ fst.comp fst)))
356      (this.comp $
357        ((fst.pair snd).comp $ fst.comp $ fst.comp $ fst.comp $ fst).pair $
358        snd.pair $ nat_div2.comp $ nat_div2.comp snd)),
359    refine ((nat_strong_rec
360      (λ a n, F a (of_nat code n)) this.to₂ $ λ a n, _).comp
id                        └──┘                   
src                          └──┘
typ                       └──┘                   
361      primrec.id $ encode_iff.2 hc).of_eq (λ a, by simp),
id                                              
typ                                             
362    simp,
363    iterate 4 {cases n with n, {refl}},
id                      
typ                     
st                                     
364    simp [G], rw [list.length_map, list.length_range],
365    let m := n.div2.div2,
id              └─────────┘
src             └─────────┘
typ             └─────────┘
366    show G₁ ((a, (list.range (n+4)).map (λ n, F a (of_nat code n))), n, m)
id                   └────────┘                                           
src                  └────────┘
typ                  └────────┘                                           
367      = some (F a (of_nat code (n+4))),
id                          └──┘  
src                          └──┘
typ                         └──┘  
368    have hm : m < n + 4, by simp [nat.div2_val, m];
id                                               
typ                                              
369    from lt_of_le_of_lt
370      (le_trans (nat.div_le_self _ _) (nat.div_le_self _ _))
371      (nat.succ_le_succ (nat.le_add_right _ _)),
372    have m1 : m.unpair.1 < n + 4, from lt_of_le_of_lt m.unpair_le_left hm,
id               └──────┘     
src              └──────┘
typ              └──────┘     
doc              └──────┘
373    have m2 : m.unpair.2 < n + 4, from lt_of_le_of_lt m.unpair_le_right hm,
id               └──────┘     
src              └──────┘
typ              └──────┘     
doc              └──────┘
374    simp [G₁], simp [list.nth_map, list.nth_range, hm, m1, m2],
375    change of_nat code (n+4) with of_nat_code (n+4),
id                   └──┘           └─────────┘  
src                  └──┘            └─────────┘
typ                  └──┘           └─────────┘  
376    simp [of_nat_code],
id           └─────────┘
src          └─────────┘
typ          └─────────┘
377    cases n.bodd; cases n.div2.bodd; refl
id           └────┘                     └──┘
src          └────┘                     └──┘
typ          └────┘                     └──┘
doc                                     └──┘
378  end
st   └─┘
379  
380  end
381  
382  section
383  open computable
384  
385  /- TODO(Mario): less copy-paste from previous proof -/
386  theorem rec_computable {α σ} [primcodable α] [primcodable σ]
id                                 └┘  └──┘       └──┘  └──┘  
src                                └┘  └──┘       └──┘  └──┘
typ                                └┘  └──┘       └──┘  └──┘  
doc                                └┘  └──┘       └──┘  └──┘
387    {c : α → code} (hc : computable c)
id             └─┘
src             └─┘
typ            └─┘
388    {z : α → σ} (hz : computable z)
id                                
typ                               
389    {s : α → σ} (hs : computable s)
id                                
typ                               
390    {l : α → σ} (hl : computable l)
id                                 
typ                                
391    {r : α → σ} (hr : computable r)
id                                
typ                               
392    {pr : α → code × code × σ × σ → σ} (hpr : computable₂ pr)
id              └──┘   └──┘         
src              └──┘   └──┘
typ             └──┘   └──┘         
393    {co : α → code × code × σ × σ → σ} (hco : computable₂ co)
id               └──┘   └──┘         
src              └──┘   └──┘
typ              └──┘   └──┘         
394    {pc : α → code × code × σ × σ → σ} (hpc : computable₂ pc)
id              └──┘   └─┘         
src              └──┘   └─┘  
typ             └──┘   └─┘         
395    {rf : α → code × σ → σ} (hrf : computable₂ rf) :
id              └──┘   
src              └──┘
typ             └──┘   
396  let PR (a) := λ cf cg hf hg, pr a (cf, cg, hf, hg),
id                  └┘   └┘ └┘          └┘  └┘  └┘
typ                 └┘   └┘ └┘          └┘  └┘  └┘
397      CO (a) := λ cf cg hf hg, co a (cf, cg, hf, hg),
id                  └┘ └┘ └┘ └┘       └┘  └┘  └┘  └┘
typ                 └┘ └┘ └┘ └┘       └┘  └┘  └┘  └┘
398      PC (a) := λ cf cg hf hg, pc a (cf, cg, hf, hg),
id                  └┘ └┘ └┘ └┘       └┘  └┘  └┘  └┘
typ                 └┘ └┘ └┘ └┘       └┘  └┘  └┘  └┘
399      RF (a) := λ cf hf, rf a (cf, hf),
id       └┘         └┘ └┘       └┘  └┘
typ      └┘         └┘ └┘       └┘  └┘
400      F (a c) : σ := nat.partrec.code.rec_on c
id                                           
typ                                          
401        (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a) in
id                                            └┘ 
typ                                           └┘ 
402      computable (λ a, F a (c a)) :=
id                           
typ                          
403  begin
404    intros,
405    let G₁ : (α × list σ) × ℕ × ℕ → option σ := λ p,
id                  └──┘              └────┘ 
src                  └──┘              └────┘
typ                 └──┘              └────┘ 
406      let a := p.1.1, IH := p.1.2, n := p.2.1, m := p.2.2 in
id                      └┘                      
typ                     └┘                      
407      (IH.nth m).bind $ λ s,
id                           
typ                          
408      (IH.nth m.unpair.1).bind $ λ s₁,
id                └─────┘             └┘
src               └─────┘
typ               └─────┘             └┘
doc               └─────┘
409      (IH.nth m.unpair.2).map $ λ s₂,
id                └─────┘            └┘
src               └─────┘
typ               └─────┘            └┘
doc               └─────┘
410      cond n.bodd
id             └───┘
src            └───┘
typ            └───┘
411        (cond n.div2.bodd
id                └───┘└───┘
src               └───┘└───┘
typ               └───┘└───┘
412          (rf a (of_nat code m, s))
413          (pc a (of_nat code m.unpair.1, of_nat code m.unpair.2, s₁, s₂)))
414        (cond n.div2.bodd
415          (co a (of_nat code m.unpair.1, of_nat code m.unpair.2, s₁, s₂))
416          (pr a (of_nat code m.unpair.1, of_nat code m.unpair.2, s₁, s₂))),
id                                                 └──┘
src                                                └──┘
typ                                                └──┘
417    have : computable G₁,
418    { refine option_bind (list_nth.comp (snd.comp fst) (snd.comp snd)) _,
419      refine option_bind ((list_nth.comp (snd.comp fst)
420        (fst.comp $ computable.unpair.comp (snd.comp snd))).comp fst) _,
421      refine option_map ((list_nth.comp (snd.comp fst)
422        (snd.comp $ computable.unpair.comp (snd.comp snd))).comp $ fst.comp fst) _,
423      have a := fst.comp (fst.comp $ fst.comp $ fst.comp fst),
424      have n := fst.comp (snd.comp $ fst.comp $ fst.comp fst),
425      have m := snd.comp (snd.comp $ fst.comp $ fst.comp fst),
426      have m₁ := fst.comp (computable.unpair.comp m),
427      have m₂ := snd.comp (computable.unpair.comp m),
428      have s := snd.comp (fst.comp fst),
429      have s₁ := snd.comp fst,
430      have s₂ := snd,
431      exact (nat_bodd.comp n).cond
432        ((nat_bodd.comp $ nat_div2.comp n).cond
433          (hrf.comp a (((computable.of_nat code).comp m).pair s))
434          (hpc.comp a (((computable.of_nat code).comp m₁).pair $
435            ((computable.of_nat code).comp m₂).pair $ s₁.pair s₂)))
436        (computable.cond (nat_bodd.comp $ nat_div2.comp n)
437          (hco.comp a (((computable.of_nat code).comp m₁).pair $
438            ((computable.of_nat code).comp m₂).pair $ s₁.pair s₂))
439          (hpr.comp a (((computable.of_nat code).comp m₁).pair $
440            ((computable.of_nat code).comp m₂).pair $ s₁.pair s₂))) },
id                                 └──┘
src                                └──┘
typ                                └──┘
st                                                                     └┘
441    let G : α → list σ → option σ := λ a IH,
id                └──┘     └────┘        └┘
src                └──┘     └────┘
typ               └──┘     └────┘        └┘
442      IH.length.cases (some (z a)) $ λ n,
id                                       
typ                                      
443      n.cases (some (s a)) $ λ n,
id                               
typ                              
444      n.cases (some (l a)) $ λ n,
id                               
typ                              
445      n.cases (some (r a)) $ λ n,
id                               
typ                              
446      G₁ ((a, IH), n, n.div2.div2),
id                        └────────┘
src                       └────────┘
typ                       └────────┘
447    have : computable₂ G := (nat_cases
448      (list_length.comp snd) (option_some_iff.2 (hz.comp fst)) $
449      nat_cases snd (option_some_iff.2 (hs.comp (fst.comp fst))) $
450      nat_cases snd (option_some_iff.2 (hl.comp (fst.comp $ fst.comp fst))) $
451      nat_cases snd (option_some_iff.2 (hr.comp (fst.comp $ fst.comp $ fst.comp fst)))
452      (this.comp $
453        ((fst.pair snd).comp $ fst.comp $ fst.comp $ fst.comp $ fst).pair $
454        snd.pair $ nat_div2.comp $ nat_div2.comp snd)),
455    refine ((nat_strong_rec
456      (λ a n, F a (of_nat code n)) this.to₂ $ λ a n, _).comp
id                        └──┘                   
src                          └──┘
typ                       └──┘                   
457      computable.id $ encode_iff.2 hc).of_eq (λ a, by simp),
id                                                 
typ                                                
458    simp,
459    iterate 4 {cases n with n, {refl}},
id                      
typ                     
st                                     
460    simp [G], rw [list.length_map, list.length_range],
461    let m := n.div2.div2,
id              └─────────┘
src             └─────────┘
typ             └─────────┘
462    show G₁ ((a, (list.range (n+4)).map (λ n, F a (of_nat code n))), n, m)
id                   └────────┘                                           
src                  └────────┘
typ                  └────────┘                                           
463      = some (F a (of_nat code (n+4))),
id                          └──┘  
src                          └──┘
typ                         └──┘  
464    have hm : m < n + 4, by simp [nat.div2_val, m];
id                                               
typ                                              
465    from lt_of_le_of_lt
466      (le_trans (nat.div_le_self _ _) (nat.div_le_self _ _))
467      (nat.succ_le_succ (nat.le_add_right _ _)),
468    have m1 : m.unpair.1 < n + 4, from lt_of_le_of_lt m.unpair_le_left hm,
id               └──────┘     
src              └──────┘
typ              └──────┘     
doc              └──────┘
469    have m2 : m.unpair.2 < n + 4, from lt_of_le_of_lt m.unpair_le_right hm,
id               └──────┘     
src              └──────┘
typ              └──────┘     
doc              └──────┘
470    simp [G₁], simp [list.nth_map, list.nth_range, hm, m1, m2],
471    change of_nat code (n+4) with of_nat_code (n+4),
id                   └──┘           └─────────┘  
src                  └──┘            └─────────┘
typ                  └──┘           └─────────┘  
472    simp [of_nat_code],
id           └─────────┘
src          └─────────┘
typ          └─────────┘
473    cases n.bodd; cases n.div2.bodd; refl
id           └────┘                     └──┘
src          └────┘                     └──┘
typ          └────┘                     └──┘
doc                                     └──┘
474  end
st   └─┘
475  
476  end
477  
478  def eval : code → ℕ →. ℕ
id              └──┘       
src             └──┘       
typ             └──┘       
479  | zero         := pure 0
id     └──┘
src    └──┘
typ    └──┘
480  | succ         := nat.succ
id     └──┘            └┘  └┘
src    └──┘            └┘  └┘
typ    └──┘            └┘  └┘
481  | left         := λ n, n.unpair.1
id     └─┘                 
src    └─┘
typ    └─┘                 
482  | right        := λ n, n.unpair.2
id     └───┘               
src    └───┘
typ    └───┘               
483  | (pair cf cg) := λ n, mkpair <$> eval cf n <*> eval cg n
id         └┘ └┘                                     
src       
typ        └┘ └┘                                     
484  | (comp cf cg) := λ n, eval cg n >>= eval cf
id      └──┘ └┘ └┘          └──┘           
src     └──┘
typ     └──┘ └┘ └┘          └──┘           
485  | (prec cf cg) := nat.unpaired (λ a n,
id      └──┘ └┘ └┘                      
src     └──┘
typ     └──┘ └┘ └┘                      
486      n.elim (eval cf a) (λ y IH, do i ← IH, eval cg (mkpair a (mkpair y i))))
id              └──┘          └┘        └┘  └──┘     └────┘   └────┘  
src                                                      └────┘    └────┘
typ             └──┘          └┘        └┘  └──┘     └────┘   └────┘  
doc                                                      └────┘    └────┘
487  | (rfind' cf)  := nat.unpaired (λ a m,
id      └────┘ └┘                       
src     └────┘
typ     └────┘ └┘                       
488      (nat.rfind (λ n, (λ m, m = 0) <$>
id                            
typ                           
489        eval cf (mkpair a (n + m)))).map (+ m))
id         └──┘                             
typ        └──┘                             
490  
491  instance : has_mem (ℕ →. ℕ) code := ⟨λ f c, eval c = f⟩
id                        └┘   └──┘                   
src                       └┘   └──┘
typ                       └┘   └──┘                   
doc                        └┘
492  
493  @[simp] theorem eval_const : ∀ n m, eval (code.const n) m = roption.some n
id                                            └┘  └┘  └┘                   
src                                            └┘  └┘  └┘
typ                                           └┘  └┘  └┘                   
doc    └──┘
494  | 0     m := rfl
495  | (n+1) m := by simp! *
496  
497  @[simp] theorem eval_id (n) : eval code.id n = roption.some n := by simp! [(<*>)]
id                                      └─────┘                 
src                                     └─────┘
typ                                     └─────┘                 
doc    └──┘
498  
499  @[simp] theorem eval_curry (c n x) : eval (curry c n) x = eval c (mkpair n x) :=
id                                                                         
typ                                                                        
doc    └──┘
500  by simp! [(<*>)]
501  
502  theorem const_prim : primrec code.const :=
id                                └┘  └┘  └┘
src                               └┘  └┘  └┘
typ                               └┘  └┘  └┘
503  (primrec.id.nat_iterate (primrec.const zero)
id                                          └──┘
src                                         └──┘
typ                                         └──┘
504    (comp_prim.comp (primrec.const succ) primrec.snd).to₂).of_eq $
id                                    └──┘
src                                   └──┘
typ                                   └──┘
505  λ n, by simp; induction n; simp [*, code.const, nat.iterate_succ']
id                                     └────────┘
src                                      └────────┘
typ                                    └────────┘
506  
507  theorem curry_prim : primrec₂ curry :=
508  comp_prim.comp primrec.fst $
509  pair_prim.comp (const_prim.comp primrec.snd) (primrec.const code.id)
id                                                               └─────┘
src                                                              └─────┘
typ                                                              └─────┘
510  
511  theorem exists_code {f : ℕ →. ℕ} : nat.partrec f ↔ ∃ c : code, eval c = f :=
id                             └┘                          └──┘          
src                            └┘                           └──┘
typ                            └┘                          └──┘          
doc                             └┘
512  ⟨λ h, begin
513    induction h,
514    case nat.partrec.zero { exact ⟨zero, rfl⟩ },
id                                    └──┘
src                                   └──┘
typ                                   └──┘
st                                               └┘
515    case nat.partrec.succ { exact ⟨succ, rfl⟩ },
id                                    └──┘
src                                   └──┘
typ                                   └──┘
st                                               └┘
516    case nat.partrec.left { exact ⟨left, rfl⟩ },
id                                    └──┘
src                                   └──┘
typ                                   └──┘
st                                               └┘
517    case nat.partrec.right { exact ⟨right, rfl⟩ },
id                                     └───┘
src                                    └───┘
typ                                    └───┘
st                                                 └┘
518    case nat.partrec.pair : f g pf pg hf hg {
519      rcases hf with ⟨cf, rfl⟩, rcases hg with ⟨cg, rfl⟩,
520      exact ⟨pair cf cg, rfl⟩ },
id              └──┘ └┘ └┘
src             └──┘
typ             └──┘ └┘ └┘
st                               └┘
521    case nat.partrec.comp : f g pf pg hf hg {
522      rcases hf with ⟨cf, rfl⟩, rcases hg with ⟨cg, rfl⟩,
523      exact ⟨comp cf cg, rfl⟩ },
id              └──┘ └┘ └┘
src             └──┘
typ             └──┘ └┘ └┘
st                               └┘
524    case nat.partrec.prec : f g pf pg hf hg {
525      rcases hf with ⟨cf, rfl⟩, rcases hg with ⟨cg, rfl⟩,
526      exact ⟨prec cf cg, rfl⟩ },
id              └──┘ └┘ └┘
src             └──┘
typ             └──┘ └┘ └┘
st                               └┘
527    case nat.partrec.rfind : f pf hf {
528      rcases hf with ⟨cf, rfl⟩,
529      refine ⟨comp (rfind' cf) (pair code.id zero), _⟩,
id               └──┘  └────┘ └┘   └──┘ └─────┘ └──┘
src              └──┘  └────┘      └──┘ └─────┘ └──┘
typ              └──┘  └────┘ └┘   └──┘ └─────┘ └──┘
530      simp [eval, (<*>), pure, pfun.pure, roption.map_id'] },
id             └──┘
src            └──┘
typ            └──┘
st                                                            └┘
531  end, λ h, begin
st   └─┘
532    rcases h with ⟨c, rfl⟩, induction c,
id                                       
typ                                      
533    case nat.partrec.code.zero { exact nat.partrec.zero },
st                                                        └┘
534    case nat.partrec.code.succ { exact nat.partrec.succ },
st                                                        └┘
535    case nat.partrec.code.left { exact nat.partrec.left },
st                                                        └┘
536    case nat.partrec.code.right { exact nat.partrec.right },
st                                                          └┘
537    case nat.partrec.code.pair : cf cg pf pg { exact pf.pair pg },
id                                                              └┘
typ                                                             └┘
st                                                                 └┘
538    case nat.partrec.code.comp : cf cg pf pg { exact pf.comp pg },
id                                                              └┘
typ                                                             └┘
st                                                                 └┘
539    case nat.partrec.code.prec : cf cg pf pg { exact pf.prec pg },
id                                                              └┘
typ                                                             └┘
st                                                                 └┘
540    case nat.partrec.code.rfind' : cf pf { exact pf.rfind' },
st                                                            └┘
541  end⟩
st   └─┘
542  
543  def evaln : ∀ k : ℕ, code → ℕ → option ℕ
id                       └──┘             
src                      └──┘             
typ                      └──┘             
544  | 0     _            := λ m, none
id                             
typ                            
545  | (k+1) zero         := λ n, guard (n ≤ k) >> pure 0
id          └──┘                       
src          └──┘
typ         └──┘                       
546  | (k+1) succ         := λ n, guard (n ≤ k) >> pure (nat.succ n)
id          └──┘                                      └──────┘ 
src          └──┘                                        └──────┘
typ         └──┘                                      └──────┘ 
547  | (k+1) left         := λ n, guard (n ≤ k) >> pure n.unpair.1
id          └──┘                                     └─────┘
src          └──┘                                        └─────┘
typ         └──┘                                     └─────┘
doc                                                      └─────┘
548  | (k+1) right        := λ n, guard (n ≤ k) >> pure n.unpair.2
id          └───┘                                    └─────┘
src          └───┘                                       └─────┘
typ         └───┘                                    └─────┘
doc                                                      └─────┘
549  | (k+1) (pair cf cg) := λ n, guard (n ≤ k) >>
id           └──┘ └┘ └┘                
src           └──┘
typ          └──┘ └┘ └┘                
550    mkpair <$> evaln (k+1) cf n <*> evaln (k+1) cg n
id                                                   
typ                                                  
551  | (k+1) (comp cf cg) := λ n, guard (n ≤ k) >>
id           └──┘ └┘ └┘                
src           └──┘
typ          └──┘ └┘ └┘                
552    do x ← evaln (k+1) cg n, evaln (k+1) cf x
id                                           
typ                                          
553  | (k+1) (prec cf cg) := λ n, guard (n ≤ k) >>
id           └──┘ └┘ └┘                
src           └──┘
typ          └──┘ └┘ └┘                
554    n.unpaired (λ a n,
id                   
typ                  
555    n.cases (evaln (k+1) cf a) $ λ y, do
id                                  
typ                                 
556      i ← evaln k (prec cf cg) (mkpair a y),
id                                        
typ                                       
557      evaln (k+1) cg (mkpair a (mkpair y i)))
id                       └────┘   └────┘  
src                      └────┘    └────┘
typ                      └────┘   └────┘  
doc                      └────┘    └────┘
558  | (k+1) (rfind' cf)  := λ n, guard (n ≤ k) >>
id           └────┘ └┘                 
src           └────┘
typ          └────┘ └┘                 
559    n.unpaired (λ a m, do
id                   
typ                  
560    x ← evaln (k+1) cf (mkpair a m),
id                                
typ                               
561    if x = 0 then pure m else
id                       
typ                      
562    evaln k (rfind' cf) (mkpair a (m+1)))
id              └────┘      └────┘   
src             └────┘      └────┘
typ             └────┘      └────┘   
doc                         └────┘
563  using_well_founded wf_tacs
id                      └─────┘
src                     └─────┘
typ                     └─────┘
doc                     └─────┘
564  
565  theorem evaln_bound : ∀ {k c n x}, x ∈ evaln k c n → n < k
id                                                   
typ                                                  
566  | 0     c n x h := by simp [evaln] at h; cases h
id                                                  
typ                                                 
567  | (k+1) c n x h := begin
568    suffices : ∀ {o : option ℕ}, x ∈ guard (n ≤ k) >> o → n < k + 1,
id                       └────┘                                
src                      └────┘
typ                      └────┘                                
569    { cases c; rw [evaln] at h; exact this h },
id             
typ            
st                                              └┘
570    simp [(>>)], exact λ _ h _, nat.lt_succ_of_le h
id                           
typ                          
571  end
st   └─┘
572  
573  theorem evaln_mono : ∀ {k₁ k₂ c n x}, k₁ ≤ k₂ → x ∈ evaln k₁ c n → x ∈ evaln k₂ c n
id                           └┘ └┘      └┘                 └┘              └┘  
typ                          └┘ └┘      └┘                 └┘              └┘  
574  | 0     k₂     c n x hl h := by simp [evaln] at h; cases h
id                                                            
typ                                                           
575  | (k+1) (k₂+1) c n x hl h := begin
576    have hl' := nat.le_of_succ_le_succ hl,
577    have : ∀ {k k₂ n x : ℕ} {o₁ o₂ : option ℕ},
578      k ≤ k₂ → (x ∈ o₁ → x ∈ o₂) → x ∈ guard (n ≤ k) >> o₁ → x ∈ guard (n ≤ k₂) >> o₂,
579    { simp [(>>)], introv h h₁ h₂ h₃, exact ⟨le_trans h₂ h, h₁ h₃⟩ },
id                                                       └┘ 
typ                                                      └┘ 
st                                                                    └┘
580    simp at h ⊢,
581    induction c with cf cg hf hg cf cg hf hg cf cg hf hg cf hf generalizing x n;
id               
typ              
582      rw [evaln] at h ⊢; refine this hl' (λ h, _) h,
583    iterate 4 {exact h},
584    { -- pair cf cg
585      simp [(<*>)] at h ⊢,
586      exact h.imp (λ a, and.imp
id                      
typ                     
587        (Exists.imp (λ b, and.imp_left (hf _ _)))
id                        
typ                       
588        (Exists.imp (λ b, and.imp_left (hg _ _)))) },
id                        
typ                       
st                                                    └┘
589    { -- comp cf cg
590      simp at h ⊢,
591      exact h.imp (λ a, and.imp (hg _ _) (hf _ _)) },
id                      
typ                     
st                                                    └┘
592    { -- prec cf cg
593      revert h, simp,
594      induction n.unpair.2; simp,
id                 └──────┘
src                └──────┘
typ                └──────┘
doc                └──────┘
595      { apply hf },
st                  └┘
596      { exact λ y h₁ h₂, ⟨y, evaln_mono hl' h₁, hg _ _ h₂⟩ } },
id                                        └─┘
typ                                       └─┘
st                                                            └──┘
597    { -- rfind' cf
598      simp at h ⊢,
599      refine h.imp (λ x, and.imp (hf _ _) _),
id                       
typ                      
600      by_cases x0 : x = 0; simp [x0],
id                     
typ                    
601      exact evaln_mono hl' }
id                        └─┘
typ                       └─┘
st                            └─
602  end
st   ──┘
603  
604  theorem evaln_sound : ∀ {k c n x}, x ∈ evaln k c n → x ∈ eval c n
id                                                         
typ                                                        
605  | 0     _ n x h := by simp [evaln] at h; cases h
id                                                  
typ                                                 
606  | (k+1) c n x h := begin
607    induction c with cf cg hf hg cf cg hf hg cf cg hf hg cf hf generalizing x n;
id               
typ              
608      simp [eval, evaln, (>>), (<*>)] at h ⊢; cases h with _ h,
609    iterate 4 {simpa [pure, pfun.pure, eq_comm] using h},
610    { -- pair cf cg
611      rcases h with ⟨_, ⟨y, ef, rfl⟩, z, eg, rfl⟩,
612      exact ⟨_, hf _ _ ef, _, hg _ _ eg, rfl⟩ },
st                                               └┘
613    { --comp hf hg
614      rcases h with ⟨y, eg, ef⟩,
615      exact ⟨_, hg _ _ eg, hf _ _ ef⟩ },
st                                       └┘
616    { -- prec cf cg
617      revert h,
618      induction n.unpair.2 with m IH generalizing x; simp,
id                 └──────┘
src                └──────┘
typ                └──────┘
doc                └──────┘
619      { apply hf },
st                  └┘
620      { refine λ y h₁ h₂, ⟨y, IH _ _, _⟩,
id                  
typ                 
621        { have := evaln_mono k.le_succ h₁,
622          simp [evaln, (>>)] at this,
623          exact this.2 },
st                        └┘
624        { exact hg _ _ h₂ } } },
st                           └────┘
625    { -- rfind' cf
626      rcases h with ⟨m, h₁, h₂⟩,
627      by_cases m0 : m = 0; simp [m0] at h₂,
id                     
typ                    
628      { exact ⟨0,
629         ⟨by simpa [m0] using hf _ _ h₁,
630          λ m, (nat.not_lt_zero _).elim⟩,
id             
typ            
631          by injection h₂ with h₂; simp [h₂]⟩ },
st                                               └┘
632      { have := evaln_sound h₂, simp [eval] at this,
id                                       └──┘
src                                      └──┘
typ                                      └──┘
633        rcases this with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩,
634        refine ⟨y+1, ⟨by simpa using hy₁, λ i im, _⟩, by simp⟩,
id                                            
typ                                           
635        cases i with i,
id               
typ              
636        { exact ⟨m, by simpa using hf _ _ h₁, m0⟩ },
id                  
typ                 
st                                                   └┘
637        { rcases hy₂ (nat.lt_of_succ_lt_succ im) with ⟨z, hz, z0⟩,
638          exact ⟨z, by simpa [nat.succ_eq_add_one] using hz, z0⟩ } } }
id                  
typ                 
st                                                                  └─────
639  end
st   ──┘
640  
641  theorem evaln_complete {c n x} : x ∈ eval c n ↔ ∃ k, x ∈ evaln k c n :=
id                                                               
src                                                
typ                                                              
642  ⟨λ h, begin
643    suffices : ∃ k, x ∈ evaln (k+1) c n,
id                                    
typ                                   
644    { exact let ⟨k, h⟩ := this in ⟨k+1, h⟩ },
id                  
typ                 
st                                            └┘
645    induction c generalizing n x;
id               
typ              
646      simp [eval, evaln, pure, pfun.pure, (<*>), (>>)] at h ⊢,
647    iterate 4 { exact ⟨⟨_, le_refl _⟩, h.symm⟩ },
648    case nat.partrec.code.pair : cf cg hf hg {
649      rcases h with ⟨x, hx, y, hy, rfl⟩,
650      rcases hf hx with ⟨k₁, hk₁⟩, rcases hg hy with ⟨k₂, hk₂⟩,
651      refine ⟨max k₁ k₂, _⟩,
id                   └┘ └┘
typ                  └┘ └┘
652      exact ⟨le_max_left_of_le $ nat.le_of_lt_succ $ evaln_bound hk₁, _,
653       ⟨_, evaln_mono (nat.succ_le_succ $ le_max_left _ _) hk₁, rfl⟩,
654        _, evaln_mono (nat.succ_le_succ $ le_max_right _ _) hk₂, rfl⟩ },
st                                                                       └┘
655    case nat.partrec.code.comp : cf cg hf hg {
656      rcases h with ⟨y, hy, hx⟩,
657      rcases hg hy with ⟨k₁, hk₁⟩, rcases hf hx with ⟨k₂, hk₂⟩,
658      refine ⟨max k₁ k₂, _⟩,
id                   └┘ └┘
typ                  └┘ └┘
659      exact ⟨le_max_left_of_le $ nat.le_of_lt_succ $ evaln_bound hk₁, _,
660        evaln_mono (nat.succ_le_succ $ le_max_left _ _) hk₁,
661        evaln_mono (nat.succ_le_succ $ le_max_right _ _) hk₂⟩ },
st                                                               └┘
662    case nat.partrec.code.prec : cf cg hf hg {
663      revert h,
664      generalize : n.unpair.1 = n₁, generalize : n.unpair.2 = n₂,
id                    └──────┘                      └──────┘
src                   └──────┘                      └──────┘
typ                   └──────┘                      └──────┘
doc                   └──────┘                      └──────┘
665      induction n₂ with m IH generalizing x n; simp,
id                 └┘
typ                └┘
666      { intro, rcases hf h with ⟨k, hk⟩,
667        exact ⟨_, le_max_left _ _,
668          evaln_mono (nat.succ_le_succ $ le_max_right _ _) hk⟩ },
st                                                                └┘
669      { intros y hy hx,
670        rcases IH hy with ⟨k₁, nk₁, hk₁⟩, rcases hg hx with ⟨k₂, hk₂⟩,
671        refine ⟨(max k₁ k₂).succ, nat.le_succ_of_le $ le_max_left_of_le $
id                      └┘ └┘ └──┘
src                           └──┘
typ                     └┘ └┘ └──┘
672          le_trans (le_max_left _ (mkpair n₁ m)) nk₁, y,
id                                    └────┘ └┘         
src                                   └────┘
typ                                   └────┘ └┘         
doc                                   └────┘
673          evaln_mono (nat.succ_le_succ $ le_max_left _ _) _,
674          evaln_mono (nat.succ_le_succ $ nat.le_succ_of_le $ le_max_right _ _) hk₂⟩,
675        simp [evaln, (>>)],
676        exact ⟨le_trans (le_max_right _ _) nk₁, hk₁⟩ } },
st                                                      └──┘
677    case nat.partrec.code.rfind' : cf hf {
678      rcases h with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩,
679      suffices : ∃ k, y + n.unpair.2 ∈ evaln (k+1) (rfind' cf)
id                                                   └────┘ └┘
src                                                    └────┘
typ                                                  └────┘ └┘
680        (mkpair n.unpair.1 n.unpair.2), {simpa [evaln, (>>)]},
id          └────┘
src         └────┘
typ         └────┘
doc         └────┘
st                                                             └┘
681      revert hy₁ hy₂, generalize : n.unpair.2 = m, intros,
id                                    └──────┘
src                                   └──────┘
typ                                   └──────┘
doc                                   └──────┘
682      induction y with y IH generalizing m; simp [evaln, (>>)],
id                 
typ                
683      { simp at hy₁, rcases hf hy₁ with ⟨k, hk⟩,
684        exact ⟨_, nat.le_of_lt_succ $ evaln_bound hk, _, hk, by simp; refl⟩ },
id                                                                       └──┘
src                                                                      └──┘
typ                                                                      └──┘
doc                                                                      └──┘
st                                                                             └┘
685      { rcases hy₂ (nat.succ_pos _) with ⟨a, ha, a0⟩,
686        rcases hf ha with ⟨k₁, hk₁⟩,
687        rcases IH m.succ
id                   └────┘
src                  └────┘
typ                  └────┘
688            (by simpa [nat.succ_eq_add_one] using hy₁)
689            (λ i hi, by simpa [nat.succ_eq_add_one] using hy₂ (nat.succ_lt_succ hi))
id                 └┘                                                             └┘
typ                └┘                                                             └┘
690          with ⟨k₂, hk₂⟩,
691        simp at hk₁,
692        exact ⟨(max k₁ k₂).succ, nat.le_succ_of_le $
id                     └┘ └┘ └──┘
src                          └──┘
typ                    └┘ └┘ └──┘
693          le_max_left_of_le $ nat.le_of_lt_succ $ evaln_bound hk₁, a,
id                                                                    
typ                                                                   
694          evaln_mono (nat.succ_le_succ $ nat.le_succ_of_le $ le_max_left _ _) hk₁,
695          by simpa [nat.succ_eq_add_one, a0, -max_eq_left, -max_eq_right] using
696            evaln_mono (nat.succ_le_succ $ le_max_right _ _) hk₂⟩ } }
st                                                                   └───
697  end, λ ⟨k, h⟩, evaln_sound h⟩
st   ──┘
698  
699  section
700  open primrec
701  
702  private def lup (L : list (list (option ℕ))) (p : ℕ × code) (n : ℕ) :=
id                        └┘    └┘    └┘  └┘             └──┘       
src                       └┘    └┘    └┘  └┘             └──┘       
typ                       └┘    └┘    └┘  └┘             └──┘       
703  do l ← L.nth (encode p), o ← l.nth n, o
id                                     
typ                                    
704  
705  private lemma hlup : primrec (λ p:_×(_×_)×_, lup p.1 p.2.1 p.2.2) :=
id                                           
src                                          
typ                                          
706  option_bind
707    (list_nth.comp fst (primrec.encode.comp $ fst.comp snd))
708    (option_bind (list_nth.comp snd $ snd.comp $ snd.comp fst) snd)
709  
710  private def G (L : list (list (option ℕ))) : option (list (option ℕ)) :=
id                        └┘    └┘    └┘         └┘  └┘    └┘    └┘   
src                       └┘    └┘    └┘         └┘  └┘    └┘    └┘   
typ                       └┘    └┘    └┘         └┘  └┘    └┘    └┘   
711  option.some $
712  let a := of_nat (ℕ × code) L.length,
id                     └──┘
src                     └──┘
typ                    └──┘
713      k := a.1, c := a.2 in
id                   
typ                  
714  (list.range k).map (λ n,
id                        
typ                       
715    k.cases none $ λ k',
id                     └┘
typ                    └┘
716    nat.partrec.code.rec_on c
id                             
typ                            
717      (some 0) -- zero
718      (some (nat.succ n))
id              └┘  └┘   
src             └┘  └┘
typ             └┘  └┘   
719      (some n.unpair.1)
id               └──┘
src               └──┘
typ              └──┘
doc               └──┘
720      (some n.unpair.2)
id               └──┘
src               └──┘
typ              └──┘
doc               └──┘
721      (λ cf cg _ _, do
id          └┘ └┘  
typ         └┘ └┘  
722        x ← lup L (k, cf) n,
id                     └┘  
typ                    └┘  
723        y ← lup L (k, cg) n,
id                     └┘  
typ                    └┘  
724        some (mkpair x y))
id               └──┘    
src              └──┘
typ              └──┘    
doc              └──┘
725      (λ cf cg _ _, do
id          └┘ └┘  
typ         └┘ └┘  
726        x ← lup L (k, cg) n,
id                     └┘  
typ                    └┘  
727        lup L (k, cf) x)
id                  └┘  
typ                 └┘  
728      (λ cf cg _ _,
id          └┘ └┘  
typ         └┘ └┘  
729        let z := n.unpair.1 in
id                 └─────┘
src                  └─────┘
typ                └─────┘
doc                  └─────┘
730        n.unpair.2.cases
id         └─────┘
src         └─────┘
typ        └─────┘
doc         └─────┘
731          (lup L (k, cf) z)
id                    └┘  
typ                   └┘  
732          (λ y, do
id              
typ             
733            i ← lup L (k', c) (mkpair z y),
id                      └┘             
typ                     └┘             
734            lup L (k, cg) (mkpair z (mkpair y i))))
id                     └┘   └────┘   └────┘  
src                           └────┘    └────┘
typ                    └┘   └────┘   └────┘  
doc                           └────┘    └────┘
735      (λ cf _,
id          └┘ 
typ         └┘ 
736        let z := n.unpair.1, m := n.unpair.2 in do
id                 └─────┘        └─────┘
src                  └─────┘          └─────┘
typ                └─────┘        └─────┘
doc                  └─────┘          └─────┘
737        x ← lup L (k, cf) (mkpair z m),
id                    └┘           
typ                   └┘           
738        x.cases
id         
typ        
739          (some m)
id                 
typ                
740          (λ _, lup L (k', c) (mkpair z (m+1)))))
id                      └┘     └────┘   
src                               └────┘
typ                     └┘     └────┘   
doc                               └────┘
741  
742  private lemma hG : primrec G :=
743  begin
744    have a := (primrec.of_nat (ℕ × code)).comp list_length,
id                                   └──┘
src                                  └──┘
typ                                  └──┘
745    have k := fst.comp a,
746    refine option_some.comp
747      (list_map (list_range.comp k) (_ : primrec _)),
748    replace k := k.comp fst, have n := snd,
749    refine nat_cases k (const none) (_ : primrec _),
id                               └──┘
src                              └──┘
typ                              └──┘
750    have k := k.comp fst, have n := n.comp fst, have k' := snd,
751    have c := snd.comp (a.comp $ fst.comp fst),
752    apply rec_prim c
753      (const (some 0))
754      (option_some.comp (primrec.succ.comp n))
755      (option_some.comp (fst.comp $ primrec.unpair.comp n))
756      (option_some.comp (snd.comp $ primrec.unpair.comp n)),
757    { have L := (fst.comp fst).comp fst,
758      have k := k.comp fst, have n := n.comp fst,
759      have cf := fst.comp snd,
760      have cg := (fst.comp snd).comp snd,
761      exact option_bind
762        (hlup.comp $ L.pair $ (k.pair cf).pair n)
763        (option_map ((hlup.comp $
764          L.pair $ (k.pair cg).pair n).comp fst)
765          (primrec₂.mkpair.comp (snd.comp fst) snd)) },
st                                                      └┘
766    { have L := (fst.comp fst).comp fst,
767      have k := k.comp fst, have n := n.comp fst,
768      have cf := fst.comp snd,
769      have cg := (fst.comp snd).comp snd,
770      exact option_bind
771        (hlup.comp $ L.pair $ (k.pair cg).pair n)
772        (hlup.comp ((L.comp fst).pair $
773          ((k.pair cf).comp fst).pair snd)) },
st                                             └┘
774    { have L := (fst.comp fst).comp fst,
775      have k := k.comp fst, have n := n.comp fst,
776      have cf := fst.comp snd,
777      have cg := (fst.comp snd).comp snd,
778      have z := fst.comp (primrec.unpair.comp n),
779      refine nat_cases
780        (snd.comp (primrec.unpair.comp n))
781        (hlup.comp $ L.pair $ (k.pair cf).pair z)
782        (_ : primrec _),
783      have L := L.comp fst, have z := z.comp fst, have y := snd,
784      refine option_bind
785        (hlup.comp $ L.pair $
786          (((k'.pair c).comp fst).comp fst).pair
787          (primrec₂.mkpair.comp z y))
788        (_ : primrec _),
789      have z := z.comp fst, have y := y.comp fst, have i := snd,
790      exact hlup.comp ((L.comp fst).pair $
791        ((k.pair cg).comp $ fst.comp fst).pair $
792        primrec₂.mkpair.comp z $ primrec₂.mkpair.comp y i) },
st                                                            └┘
793    { have L := (fst.comp fst).comp fst,
794      have k := k.comp fst, have n := n.comp fst,
795      have cf := fst.comp snd,
796      have z := fst.comp (primrec.unpair.comp n),
797      have m := snd.comp (primrec.unpair.comp n),
798      refine option_bind
799        (hlup.comp $ L.pair $ (k.pair cf).pair (primrec₂.mkpair.comp z m))
800        (_ : primrec _),
801      have m := m.comp fst,
802      exact nat_cases snd (option_some.comp m)
803        ((hlup.comp ((L.comp fst).pair $
804          ((k'.pair c).comp $ fst.comp fst).pair
805          (primrec₂.mkpair.comp (z.comp fst)
806            (primrec.succ.comp m)))).comp fst) }
st                                                └─
807  end
st   ──┘
808  
809  private lemma evaln_map (k c n) :
810    (((list.range k).nth n).map (evaln k c)).bind (λ b, b) = evaln k c n :=
id                                                                
typ                                                               
811  begin
812    by_cases kn : n < k,
813    { simp [list.nth_range kn] },
id                            └┘
typ                           └┘
st                                └┘
814    { rw list.nth_len_le,
815      { cases e : evaln k c n, {refl},
id                           
typ                          
st                                     └┘
816        exact kn.elim (evaln_bound e) },
st                                       └┘
817      simpa using kn }
id                   └┘
typ                  └┘
st                      └─
818  end
st   ──┘
819  
820  theorem evaln_prim : primrec (λ (a : (ℕ × code) × ℕ), evaln a.1.1 a.1.2 a.2) :=
id                                           └──┘    
src                                          └──┘    
typ                                          └──┘    
821  have primrec₂ (λ (_:unit) (n : ℕ),
id                       └──┘       
src                      └──┘       
typ                      └──┘       
doc                      └──┘
822    let a := of_nat (ℕ × code) n in
id                        └──┘  
src                        └──┘
typ                       └──┘  
823    (list.range a.1).map (evaln a.1 a.2)), from
id                                
typ                               
824  primrec.nat_strong_rec _ (hG.comp snd).to₂ $
825    λ _ p, begin
id        
typ       
826      simp [G],
827      rw (_ : (of_nat (ℕ × code) _).snd =
id                          
src                         
typ                         
828        of_nat code p.unpair.2), swap, {simp},
id                └──┘ └──────┘
src               └──┘ └──────┘
typ               └──┘ └──────┘
doc                    └──────┘
st                                             └┘
829      apply list.map_congr (λ n, _),
id                               
typ                              
830      rw (by simp : list.range p = list.range
831        (mkpair p.unpair.1 (encode (of_nat code p.unpair.2)))),
id          └────┘                            └──┘
src         └────┘                            └──┘
typ         └────┘                            └──┘
doc         └────┘
832      generalize : p.unpair.1 = k,
id                    └──────┘
src                   └──────┘
typ                   └──────┘
doc                   └──────┘
833      generalize : of_nat code p.unpair.2 = c,
id                           └──┘ └──────┘
src                          └──┘ └──────┘
typ                          └──┘ └──────┘
doc                               └──────┘
834      intro nk,
835      cases k with k', {simp [evaln]},
id             
typ            
st                                     └┘
836      let k := k'+1, change k'.succ with k,
id                └┘           └─────┘      
src                            └─────┘
typ               └┘           └─────┘      
837      simp [nat.lt_succ_iff] at nk,
838      have hg : ∀ {k' c' n},
id                    └┘ └┘ 
typ                   └┘ └┘ 
839        mkpair k' (encode c') < mkpair k (encode c) →
840        lup ((list.range (mkpair k (encode c))).map (λ n,
id                                                      
typ                                                     
841          (list.range n.unpair.1).map
842            (evaln n.unpair.1 (of_nat code n.unpair.2))))
id                                       └──┘
src                                      └──┘
typ                                      └──┘
843          (k', c') n = evaln k' c' n,
844      { intros k₁ c₁ n₁ hl,
845        simp [lup, list.nth_range hl, evaln_map, (>>=)] },
st                                                         └┘
846      cases c with cf cg cf cg cf cg cf;
id             
typ            
847        simp [evaln, nk, (>>), (>>=), (<$>), (<*>), pure],
848      { cases encode_lt_pair cf cg with lf lg,
id                              └┘ └┘
typ                             └┘ └┘
849        rw [hg (nat.mkpair_lt_mkpair_right _ lf),
850            hg (nat.mkpair_lt_mkpair_right _ lg)],
851        cases evaln k cf n, {refl},
id                      └┘ 
typ                     └┘ 
st                                  └┘
852        cases evaln k cg n; refl },
id                      └┘   └──┘
src                            └──┘
typ                     └┘   └──┘
doc                            └──┘
st                                  └┘
853      { cases encode_lt_comp cf cg with lf lg,
id                              └┘ └┘
typ                             └┘ └┘
854        rw hg (nat.mkpair_lt_mkpair_right _ lg),
855        cases evaln k cg n, {refl},
id                      └┘ 
typ                     └┘ 
st                                  └┘
856        simp [hg (nat.mkpair_lt_mkpair_right _ lf)] },
st                                                     └┘
857      { cases encode_lt_prec cf cg with lf lg,
id                              └┘ └┘
typ                             └┘ └┘
858        rw hg (nat.mkpair_lt_mkpair_right _ lf),
859        cases n.unpair.2, {refl},
id               └──────┘
src              └──────┘
typ              └──────┘
doc              └──────┘
st                                └┘
860        simp,
861        rw hg (nat.mkpair_lt_mkpair_left _ k'.lt_succ_self),
862        cases evaln k' _ _, {refl},
id                     └┘
typ                    └┘
st                                  └┘
863        simp [hg (nat.mkpair_lt_mkpair_right _ lg)] },
st                                                     └┘
864      { have lf := encode_lt_rfind' cf,
id                                     └┘
typ                                    └┘
865        rw hg (nat.mkpair_lt_mkpair_right _ lf),
866        cases evaln k cf n with x, {refl},
id                      └┘ 
typ                     └┘ 
st                                         └┘
867        simp,
868        cases x; simp [nat.succ_ne_zero],
id               
typ              
869        rw hg (nat.mkpair_lt_mkpair_left _ k'.lt_succ_self) }
st                                                             └┘
870    end,
st     └─┘
871  (option_bind (list_nth.comp
872    (this.comp (const ()) (encode_iff.2 fst)) snd)
id                       └┘
src                      └┘
typ                      └┘
873    snd.to₂).of_eq $ λ ⟨⟨k, c⟩, n⟩, by simp [evaln_map]
874  
875  end
876  
877  section
878  open partrec computable
879  
880  theorem eval_eq_rfind_opt (c n) :
881    eval c n = nat.rfind_opt (λ k, evaln k c n) :=
id                                         
typ                                        
882  roption.ext $ λ x, begin
id                   
typ                  
883    refine evaln_complete.trans (nat.rfind_opt_mono _).symm,
884    intros a m n hl, apply evaln_mono hl,
id                                       └┘
typ                                      └┘
885  end
st   └─┘
886  
887  theorem eval_part : partrec₂ eval :=
888  (rfind_opt (evaln_prim.to_comp.comp
889    ((snd.pair (fst.comp fst)).pair (snd.comp fst))).to₂).of_eq $
890  λ a, by simp [eval_eq_rfind_opt]
id     
typ    
891  
892  theorem fixed_point
893    {f : code → code} (hf : computable f) : ∃ c : code, eval (f c) = eval c :=
id          └──┘   └──┘                             └──┘                  
src         └──┘   └──┘                              └──┘
typ         └──┘   └──┘                             └──┘                  
894  let g (x y : ℕ) : roption ℕ :=
id                            
src                           
typ                           
895    eval (of_nat code x) x >>= λ b, eval (of_nat code b) y in
id                  └──┘                         └──┘   
src                 └──┘                            └──┘
typ                 └──┘                         └──┘   
896  have partrec₂ g :=
897    (eval_part.comp ((computable.of_nat _).comp fst) fst).bind
898    (eval_part.comp ((computable.of_nat _).comp snd) (snd.comp fst)).to₂,
899  let ⟨cg, eg⟩ := exists_code.1 this in
id        └┘
typ       └┘
900  have eg' : ∀ a n, eval cg (mkpair a n) = roption.map encode (g a n) :=
id                                                               
typ                                                              
901    by simp [eg],
902  let F (x : ℕ) : code := f (curry cg x) in
id                  └──┘               
src                 └──┘
typ                 └──┘               
903  have computable F :=
id                   
typ                  
904    hf.comp (curry_prim.comp (primrec.const cg) primrec.id).to_comp,
905  let ⟨cF, eF⟩ := exists_code.1 this in
id        └┘
typ       └┘
906  have eF' : eval cF (encode cF) = roption.some (encode (F (encode cF))),
id                                                          
typ                                                         
907    by simp [eF],
908  ⟨curry cg (encode cF), funext (λ n,
id                                    
typ                                   
909    show eval (f (curry cg (encode cF))) n = eval (curry cg (encode cF)) n,
id                                                                        
typ                                                                       
910    by simp [eg', eF', roption.map_id', g])⟩
id                                         
typ                                        
911  
912  theorem fixed_point₂
913    {f : code → ℕ →. ℕ} (hf : partrec₂ f) : ∃ c : code, eval c = f c :=
id          └──┘    └┘                            └──┘           
src         └──┘    └┘                             └──┘
typ         └──┘    └┘                            └──┘           
doc                  └┘
914  let ⟨cf, ef⟩ := exists_code.1 hf in
id        └┘
typ       └┘
915  (fixed_point (curry_prim.comp
916    (primrec.const cf) primrec.encode).to_comp).imp $
917  λ c e, funext $ λ n, by simp [e.symm, ef, roption.map_id']
id                    
typ                   
918  
919  end
920  
921  end nat.partrec.code